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.
2007-09-05 wenzelm 2007-09-05 use preferences.ML: do setmp *here*, to capture intended default values;
2007-09-05 wenzelm 2007-09-05 tuned;
2007-09-05 urbanc 2007-09-05 modified proofs so that they are not using claset()
2007-09-04 nipkow 2007-09-04 tuned lemma; replaced !! by arbitrary
2007-09-04 ballarin 2007-09-04 Improved comment.
2007-09-03 krauss 2007-09-03 Documented function package in IsarRef-manual.
2007-09-03 nipkow 2007-09-03 added variations on infinite descent
2007-09-03 haftmann 2007-09-03 fixed Rat.inv
2007-09-03 haftmann 2007-09-03 fixed Rat.inv
2007-09-02 huffman 2007-09-02 fix sgn_div_norm class
2007-09-02 urbanc 2007-09-02 made theorem-references safe
2007-09-01 wenzelm 2007-09-01 removed unused join_mode; standard_typ_check: proper prepare_patternT, which rejects schematic type vars in non-patterns;
2007-09-01 wenzelm 2007-09-01 read_def_terms: replaced full Syntax.check_typs by certify_typ, to workaround problems with illegal schematic type vars;
2007-09-01 wenzelm 2007-09-01 removed obsolete ML bindings;
2007-09-01 wenzelm 2007-09-01 linorder_neqE_ordered_idom: proper proof, avoid illegal schematic type vars;
2007-09-01 wenzelm 2007-09-01 mono_Int/Un: proper proof, avoid illegal schematic type vars; removed obsolete ML bindings;