2007-09-15 haftmann 2007-09-15 clarified class interfaces and internals
2007-09-15 haftmann 2007-09-15 introduced classes
2007-09-15 haftmann 2007-09-15 multi-functional value keyword
2007-09-15 haftmann 2007-09-15 added lemmas for finiteness
2007-09-15 haftmann 2007-09-15 tuned
2007-09-15 haftmann 2007-09-15 fixed title
2007-09-15 wenzelm 2007-09-15 replaced Symbol.is_hex_letter to Symbol.is_ascii_hex;
2007-09-15 wenzelm 2007-09-15 ML_Lex.keywords; tuned comments;
2007-09-15 wenzelm 2007-09-15 tuned comments;
2007-09-15 wenzelm 2007-09-15 replaced Symbol.is_hex_letter to Symbol.is_ascii_hex; tuned Symbol.is_ascii_blank (according to SML syntax);
2007-09-15 wenzelm 2007-09-15 Lexical syntax for SML.
2007-09-15 wenzelm 2007-09-15 added ML/ml_lex.ML;
2007-09-15 wenzelm 2007-09-15 removed redundant OuterLex.make_lexicon;
2007-09-14 krauss 2007-09-14 lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
2007-09-14 krauss 2007-09-14 added "<*mlex*>" which lexicographically combines a measure function with a relation
2007-09-14 wenzelm 2007-09-14 moved ML_XXX.ML files to Pure/ML;
2007-09-14 paulson 2007-09-14 tidied
2007-09-14 urbanc 2007-09-14 reverted back to the old version of the equivariance lemma for ALL
2007-09-13 urbanc 2007-09-13 some cleaning up to do with contexts
2007-09-13 berghofe 2007-09-13 Generalized equivariance and nominal_inductive commands to inductive definitions involving arbitrary monotone operators.
2007-09-13 berghofe 2007-09-13 Added equivariance lemmas for induct_forall.
2007-09-13 berghofe 2007-09-13 Added equivariance lemma for induct_implies.
2007-09-11 webertj 2007-09-11 typo fixed, dead link removed
2007-09-10 nipkow 2007-09-10 added lemma
2007-09-10 berghofe 2007-09-10 Auto quickcheck now displays counterexample using Proof.goal_message rather than producing an error message.
2007-09-08 wenzelm 2007-09-08 added String.isSubstring;
2007-09-08 wenzelm 2007-09-08 export is_finished; added thy_ord (based on update_time); begin_thy/register_thy: more precise handling of update_time;
2007-09-08 wenzelm 2007-09-08 Present.session_name;
2007-09-08 wenzelm 2007-09-08 tuned signature; tuned message;
2007-09-08 wenzelm 2007-09-08 thy_deps: ThyInfo.thy_ord, improved dir/unfold entry;
2007-09-08 wenzelm 2007-09-08 removed thy_ord (erratic due to multi-threading);
2007-09-08 urbanc 2007-09-08 some cleaning up
2007-09-07 wenzelm 2007-09-07 theorem: apply hook last;
2007-09-07 wenzelm 2007-09-07 reset goal messages after goal update;
2007-09-07 wenzelm 2007-09-07 added hilite markup;
2007-09-07 wenzelm 2007-09-07 fixed type alias in signature;
2007-09-07 nipkow 2007-09-07 added lemma
2007-09-07 paulson 2007-09-07 allow TVars during type inference
2007-09-07 paulson 2007-09-07 tidied the proofs
2007-09-07 wenzelm 2007-09-07 made smlnj happy;
2007-09-06 paulson 2007-09-06 new fun declaration
2007-09-06 paulson 2007-09-06 Auto-config of E_HOME, SPASS_HOME, VAMPIRE_HOME
2007-09-06 paulson 2007-09-06 Vampire structured proofs. Better parsing; some bug fixes.
2007-09-06 paulson 2007-09-06 chained facts are now included
2007-09-06 paulson 2007-09-06 new proofs found
2007-09-06 urbanc 2007-09-06 trivial cleaning up
2007-09-06 wenzelm 2007-09-06 added goal_message;
2007-09-06 wenzelm 2007-09-06 theorem hooks: apply in declaration order;
2007-09-06 berghofe 2007-09-06 Generalized code generator for numerals.
2007-09-06 berghofe 2007-09-06 - New theories Lambda/NormalForm and Lambda/Standardization - Integrated Executable_Rat and Executable_Real theories into Rational and RealDef theories
2007-09-06 berghofe 2007-09-06 Added lecture notes by Matthes and Loader.
2007-09-06 berghofe 2007-09-06 New proof of standardization theorem (inspired by Ralph Matthes).
2007-09-06 berghofe 2007-09-06 Definition of normal forms (taken from theory WeakNorm).
2007-09-06 berghofe 2007-09-06 Moved definition of normal forms to new NormalForm theory.
2007-09-06 berghofe 2007-09-06 Added Standardization theory.
2007-09-06 berghofe 2007-09-06 New code generator setup (taken from Library/Executable_Real.thy, also works for old code generator).
2007-09-06 berghofe 2007-09-06 Added code generator setup (taken from Library/Executable_Rat.thy, also works for old code generator).
2007-09-06 berghofe 2007-09-06 Integrated code generator setup into RealDef theory.
2007-09-06 berghofe 2007-09-06 Integrated code generator setup into Rational theory.
2007-09-06 berghofe 2007-09-06 Integrated Executable_Rat and Executable_Real theories into Rational and RealDef theories.