isabelle update -u control_cartouches;

isabelle update -u control_cartouches;

eliminated unused simproc identifier;

tuned syntax -- more symbols;

simplified simproc programming interfaces;

slightly more formal historic examples;

proper context;
tuned whitespace;

integrated appendix theory into main theory;
tuned ML

--HG--
extra : rebase_source : a066b231916d8839dd4199f5a608ee49e36e9fd9

tuned signature -- removed obsolete Addsimprocs, Delsimprocs;

simplifier uses proper Proof.context instead of historic type simpset;

dropped unused argument – avoids problem with SML/NJ

renamed trace_simp to simp_trace, and debug_simp to simp_debug;

eliminated dead code;

more conventional exceptions for abstract syntax operations -- eliminated ancient SYS_ERROR;
proper signature constraint;

renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;

more antiquotations;
eliminated legacy ML bindings;

modernized structure Term_Ord;

modernized structures;

numeral syntax: clarify parse trees vs. actual terms;
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};

prefer explicit @{lemma} over adhoc forward reasoning;

explicitly qualify Drule.standard;

more @{theory} antiquotations;

renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;

eliminated global SIMPSET, CLASET etc. -- refer to explicit context;

moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
tuned signature of structure Term;

converted ML proofs;

OldGoals.inst;

tuned ML code, more antiquotations;

removed unnecessary theory qualifiers;

Made theory names in ZF disjoint from HOL theory names to allow loading both developments
in a single session (but not merge them).

modernized specifications;
removed legacy ML bindings;

simplified type int (eliminated IntInf.int, integer);

moved Integ files to canonical place;