avoid pending shyps in global theory facts;

more rules for numeral conversions;
more precise code setup for pred_numeral

ran isabelle update_op on all sources

cleaned up and tuned

--HG--
extra : rebase_source : a1262817f08e7c73c1f578e8c3b21fcf9314f1fb

tuned some proofs and added some lemmas

--HG--
extra : rebase_source : ad93f195ceb7a124396a911453e61f00f52999be

Printing natural numbers as numerals in evaluation

--HG--
extra : amend_source : d893fca71b1eff819db8901dfa1a670f16a5dc0e

de-orphanized declaration

transfer lifting rule for numeral

--HG--
extra : rebase_source : bafc2cb3fd6a49a365472e2fb15a4de692ec874d

tuned

misc tuning and modernization;

model characters directly as range 0..255
* * *
operate on syntax terms rather than asts

tuned bootstrap order to provide type classes in a more sensible order

--HG--
extra : rebase_source : b4008b5f377525bc1866d515a16702fbb0b463c9

dropped various legacy fact bindings

prefer symbols for "abs";

isabelle update_cartouches -c -t;

add various lemmas

tuned proofs -- less legacy;

isabelle update_cartouches;

tuned signature;

given up separate type classes demanding `inverse 0 = 0`

Thm.cterm_of and Thm.ctyp_of operate on local context;

modernized header uniformly as section;

moved lemmas out of Int.thy which have nothing to do with int

--HG--
extra : rebase_source : a6db16c774c1c078a2ed1a129509da61fa662a39

discontinued old "xnum" token category;
simplified Lexicon.read_num, Lexicon.read_float: no sign here;
express ZF numerals via "num" with mixfix grammar;
recovered printing of ZF numerals: "one" is abbreviation;

explicit separation of signed and unsigned numerals using existing lexical categories num and xnum

updated news

tuned imports

use 'datatype_new' in 'Main'

renamed BNF theories

--HG--
rename : src/HOL/BNF_Comp.thy => src/HOL/BNF_Composition.thy
rename : src/HOL/BNF_FP_Base.thy => src/HOL/BNF_Fixpoint_Base.thy
rename : src/HOL/BNF_GFP.thy => src/HOL/BNF_Greatest_Fixpoint.thy
rename : src/HOL/BNF_LFP.thy => src/HOL/BNF_Least_Fixpoint.thy

renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place

--HG--
rename : src/HOL/Datatype.thy => src/HOL/Old_Datatype.thy
rename : src/HOL/Tools/Function/size.ML => src/HOL/Tools/Function/old_size.ML
rename : src/HOL/Tools/Datatype/datatype.ML => src/HOL/Tools/Old_Datatype/old_datatype.ML
rename : src/HOL/Tools/Datatype/datatype_aux.ML => src/HOL/Tools/Old_Datatype/old_datatype_aux.ML
rename : src/HOL/Tools/Datatype/datatype_codegen.ML => src/HOL/Tools/Old_Datatype/old_datatype_codegen.ML
rename : src/HOL/Tools/Datatype/datatype_data.ML => src/HOL/Tools/Old_Datatype/old_datatype_data.ML
rename : src/HOL/Tools/Datatype/datatype_prop.ML => src/HOL/Tools/Old_Datatype/old_datatype_prop.ML
rename : src/HOL/Tools/Datatype/datatype_realizer.ML => src/HOL/Tools/Old_Datatype/old_datatype_realizer.ML
rename : src/HOL/Tools/Datatype/primrec.ML => src/HOL/Tools/Old_Datatype/old_primrec.ML
rename : src/HOL/Tools/Datatype/rep_datatype.ML => src/HOL/Tools/Old_Datatype/old_rep_datatype.ML

reduced name variants for assoc and commute on plus and mult

more official const syntax: avoid educated guessing by Syntax_Phases.decode_term;

renamed old 'primrec' to 'old_primrec' (until the new 'primrec' can be moved above 'Nat' in the theory dependencies)

renamed 'nat_{case,rec}' to '{case,rec}_nat'

eliminiated neg_numeral in favour of - (numeral _)

streamlined setup of linear arithmetic

more simplification rules on unary and binary minus

--HG--
extra : rebase_source : 7c88c9f33c4be8eae76f508a1a73ba79c8b769b1

generalized sort constraint of lemmas

migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier

--HG--
extra : rebase_source : ff8027ac9606264aa4b2d4f8da037c426a3db98b

more explicit Printer.type_emphasis, depending on show_type_emphasis;
tuned signature;

tuned;

syntax translations always depend on context;

two target language numeral types: integer and natural, as replacement for code_numeral;
former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral;
refined stack of theories implementing int and/or nat by target language numerals;
reduced number of target language numeral types to exactly one

--HG--
extra : rebase_source : ffa0242ad108fe680ff144a716257c0784285d17

sharing of recursive results on evaluation

Renamed {left,right}_distrib to distrib_{right,left}.

more explicit show_type_constraint, show_sort_constraint;

prefer ML_file over old uses;

remove unnecessary qualifiers on names

add lemma Suc_1

removed Nat_Numeral.thy, moving all theorems elsewhere

load Tools/numeral.ML in Num.thy

tuned proof

set up numeral reorient simproc in Num.thy

replace lemmas eval_nat_numeral with a simpler reformulation

new lemmas for simplifying subtraction on nat numerals

move more theorems from Nat_Numeral.thy to Num.thy

fix search-and-replace errors

--HG--
extra : transplant_source : %23%E0%CF%2C%AB%B0%A9%F3%CF1%E2%04ophV%BA%7E7C

add constant pred_numeral k = numeral k - (1::nat);
replace several simp rules from Nat_Numeral.thy with new ones that use pred_numeral

move lemmas from Nat_Numeral to Int.thy and Num.thy

move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy

bootstrap Num.thy before Power.thy;
move lemmas about powers into Power.thy

fix incorrect code_modulename declarations

merged fork with new numeral representation (see NEWS)