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 ***

final(?) iteration of sgn saga.

reject_vars: accept type-inference params; standard_term_check: include prepare_pattern; infer_type: mode_schematic; tuned;

exported is_param;

legacy_infer_term: ProofContext.mode_schematic;

prove: setmp quick_and_dirty (avoids race condition);

export various inner syntax modes; Syntax.add_term_check: include expand_abbrevs (consts and var bindings);

type_infer: mode_pattern;

do not touch quick_and_dirty;

tuned multithreading entry -- no longer experimental;

explained \isatstyle(minor)

added short_names explanation

added join_mode; expand_binds: mode dependent; removed infer_types(_pat) -- use general Syntax.check_terms instead;

replaced ProofContext.infer_types by general Syntax.check_terms; use Variable.polymorphic to get schematic type variables;

replaced ProofContext.infer_types by general Syntax.check_terms;

*** empty log message ***

added constant sgn

added lemma

added some more entries;

turned type_check into separate typ/term_check; tuned sifnature;

tuned;

moved type_mode to type.ML; Syntax.add_typ_check;

infer_types: general check_typs instead of Type.cert_typ_mode;

maintain mode in context (get/set/restore_mode);

added burrow_types;

- tuned section about inductive predicates - fixed broken railroad diagram in section about executable code

ported div/mod simprocs from HOL/ex/Binary.thy

renamed POLYML_LINK_OPTIONS to POLY_LINK_OPTIONS;

added POLYML_LINK_OPTIONS, which is required for unusual platforms (notably cygwin);

some simultaneous use_thys;

Updated section about inductive definitions.

turned list comprehension translations into ML to optimize base case

added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);

added x86-solaris;

fixed Proofs

added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);

removed unused theorems ; added lifting properties for foldr and foldl

removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);

Deleted unused fillin_mixfix function.

mark all parallel sessions as experimental