2002-05-17 nipkow 2002-05-17 *** empty log message ***
2002-05-17 nipkow 2002-05-17 allowed more general split rules to cope with div/mod 2
2002-05-17 nipkow 2002-05-17 Used to be Divides.ML
2002-05-16 paulson 2002-05-16 converting Ordinal.ML to Isar format
2002-05-15 nipkow 2002-05-15 Set up arith to deal with div 2 and mod 2.
2002-05-15 nipkow 2002-05-15 arith can now deal with div 2 and mod 2.
2002-05-15 nipkow 2002-05-15 Divides.ML -> Divides_lemmas.ML Converted Divides.thy to Isar.
2002-05-15 nipkow 2002-05-15 Removed superfluous thm
2002-05-15 paulson 2002-05-15 better error messages for datatypes not declared Const
2002-05-15 paulson 2002-05-15 better simplification of trivial existential equalities
2002-05-14 kleing 2002-05-14 numerals work again
2002-05-13 nipkow 2002-05-13 *** empty log message ***
2002-05-13 nipkow 2002-05-13 *** empty log message ***
2002-05-13 nipkow 2002-05-13 *** empty log message ***
2002-05-13 paulson 2002-05-13 quotes around types
2002-05-13 paulson 2002-05-13 Deleting two simprules saves 21 seconds!
2002-05-13 wenzelm 2002-05-13 tuned document;
2002-05-13 wenzelm 2002-05-13 updated X-Symbol URL;
2002-05-13 paulson 2002-05-13 converted Order.ML OrderType.ML OrderArith.ML to Isar format
2002-05-11 kleing 2002-05-11 fix for change in nat number simplification
2002-05-11 berghofe 2002-05-11 - Tuned function mk_cnstrts - Added function prop_of
2002-05-10 paulson 2002-05-10 conversion of AC branch to Isar
2002-05-10 paulson 2002-05-10 obsolete ML files
2002-05-10 paulson 2002-05-10 now-obsolete ML files
2002-05-10 paulson 2002-05-10 converted the AC branch to Isar
2002-05-10 nipkow 2002-05-10 A new theory of pointer program examples
2002-05-10 nipkow 2002-05-10 Added Pointers.thy
2002-05-10 nipkow 2002-05-10 *** empty log message ***
2002-05-10 nipkow 2002-05-10 commented out half converted proof
2002-05-10 nipkow 2002-05-10 added dep on IMP/Compiler0
2002-05-10 paulson 2002-05-10 tidied
2002-05-09 paulson 2002-05-09 Cambridge
2002-05-09 paulson 2002-05-09 fixed simproc bug
2002-05-09 paulson 2002-05-09 ordinal addition now coerces its arguments to ordinals
2002-05-08 nipkow 2002-05-08 new thm distinct_conv_nth
2002-05-08 paulson 2002-05-08 isar conversion
2002-05-08 wenzelm 2002-05-08 oops;
2002-05-08 paulson 2002-05-08 the new predicate "relation"
2002-05-08 paulson 2002-05-08 tidied
2002-05-08 paulson 2002-05-08 better xsymbol syntax
2002-05-08 paulson 2002-05-08 new lemmas
2002-05-08 paulson 2002-05-08 some ex files converted to Isar
2002-05-08 paulson 2002-05-08 converted to Isar
2002-05-08 paulson 2002-05-08 Tidied and converted to Isar by lcp
2002-05-07 wenzelm 2002-05-07 converted;
2002-05-07 wenzelm 2002-05-07 rev_bexI [intro?];
2002-05-07 nipkow 2002-05-07 a bit of conversion to structured proofs
2002-05-07 nipkow 2002-05-07 *** empty log message ***
2002-05-07 wenzelm 2002-05-07 be liberal about missing types;
2002-05-07 nipkow 2002-05-07 *** empty log message ***
2002-05-07 wenzelm 2002-05-07 tuned;
2002-05-07 wenzelm 2002-05-07 tuned presentation;
2002-05-07 wenzelm 2002-05-07 \documentclass{report};
2002-05-07 wenzelm 2002-05-07 use eq_thm_prop instead of slightly inadequate eq_thm;
2002-05-07 wenzelm 2002-05-07 clarified eq_thm; added eq_thm_prop;
2002-05-06 nipkow 2002-05-06 Added insert_disjoint and disjoint_insert [simp], and simplified proofs
2002-05-04 berghofe 2002-05-04 Added skeletons to speed up rewriting on proof terms.
2002-04-30 kleing 2002-04-30 tuned
2002-04-30 kleing 2002-04-30 physical location of isabelle repository is now sunbroy2
2002-04-29 prensani 2002-04-29 added abstract;corrected RG_Basic Hoare rule.