Moved definition of normal forms to new NormalForm theory.

Added Standardization theory.

New code generator setup (taken from Library/Executable_Real.thy, also works for old code generator).

Added code generator setup (taken from Library/Executable_Rat.thy, also works for old code generator).

Integrated code generator setup into RealDef theory.

Integrated code generator setup into Rational theory.

Integrated Executable_Rat and Executable_Real theories into Rational and RealDef theories.

use preferences.ML: do setmp *here*, to capture intended default values;

tuned;

modified proofs so that they are not using claset()

tuned lemma; replaced !! by arbitrary

Improved comment.

Documented function package in IsarRef-manual.

added variations on infinite descent

fixed Rat.inv

fixed Rat.inv

fix sgn_div_norm class

made theorem-references safe

removed unused join_mode; standard_typ_check: proper prepare_patternT, which rejects schematic type vars in non-patterns;

read_def_terms: replaced full Syntax.check_typs by certify_typ, to workaround problems with illegal schematic type vars;

removed obsolete ML bindings;

linorder_neqE_ordered_idom: proper proof, avoid illegal schematic type vars;

mono_Int/Un: proper proof, avoid illegal schematic type vars; removed obsolete ML bindings;

removed spurious Toplevel.debug, which actually makes Poly/ML crash in certain situations;

added singleton check_typ/term/prop;

removed obsolete read/cert variations (cf. Syntax.read/check);

replaced ProofContext.cert_term/prop by general Syntax.check_term/prop (which also includes type-inference);

replaced ProofContext.read_term/prop by general Syntax.read_term/prop; replaced ProofContext.cert_term/prop by general Syntax.check_term/prop (which also includes type-inference);

replaced ProofContext.read_term/prop by general Syntax.read_term/prop;

*** empty log message ***