2003-03-10 paulson 2003-03-10 spelling
2003-03-06 paulson 2003-03-06 new UNITY examples theory
2003-03-06 paulson 2003-03-06 new logical equivalences
2003-03-06 paulson 2003-03-06 new simprule for int (nat n) and consequential changes
2003-03-06 kleing 2003-03-06 link to devel snapshot
2003-03-06 kleing 2003-03-06 obsolete
2003-03-05 paulson 2003-03-05 new examples theory
2003-03-02 kleing 2003-03-02 get cvs to change modified time for session.tex
2003-03-01 kleing 2003-03-01 typo
2003-03-01 kleing 2003-03-01 added exercises
2003-03-01 kleing 2003-03-01 added Exercises
2003-03-01 kleing 2003-03-01 keep a copy of generated files in repository
2003-03-01 kleing 2003-03-01 keep a copy of generated files in repository
2003-02-28 isatest 2003-02-28 generate nightly devel snapshot
2003-02-28 isatest 2003-02-28 case distinction on host for makefile flags
2003-02-27 paulson 2003-02-27 Reorganized, moving many results about the integer dvd relation from IntPrimes to main HOL (IntDiv)
2003-02-27 paulson 2003-02-27 restored some deleted lemmas
2003-02-27 ballarin 2003-02-27 Change to meta simplifier: congruence rules may now have frees as head of term.
2003-02-26 kleing 2003-02-26 == -> =
2003-02-26 paulson 2003-02-26 zprime_def fixes by Jeremy Avigad
2003-02-26 paulson 2003-02-26 completed proofs for programs consisting of a single assignment
2003-02-26 paulson 2003-02-26 new lemma
2003-02-26 paulson 2003-02-26 some x-symbols and some new lemmas
2003-02-25 nipkow 2003-02-25 *** empty log message ***
2003-02-25 nipkow 2003-02-25 added simp_depth_limit
2003-02-25 berghofe 2003-02-25 Documented prf / full_prf commands and antiquotations.
2003-02-25 nipkow 2003-02-25 Undid eta change for UN/INT.
2003-02-20 paulson 2003-02-20 new inverse image lemmas
2003-02-20 paulson 2003-02-20 minor updates to pre-2002 release
2003-02-19 paulson 2003-02-19 fixed anomalies in the installed classical rules
2003-02-18 kleing 2003-02-18 check maxs in defensive machine
2003-02-18 paulson 2003-02-18 new theory Transformers: Meier-Sanders non-interference theory
2003-02-17 mehta 2003-02-17 Proof of the Schorr-Waite graph marking algorithm.
2003-02-16 paulson 2003-02-16 minor revisions
2003-02-16 paulson 2003-02-16 new theorem Compl_partition2
2003-02-14 ballarin 2003-02-14 Product operator added --- preliminary.
2003-02-12 kleing 2003-02-12 favicon
2003-02-11 nipkow 2003-02-11 *** empty log message ***
2003-02-10 nipkow 2003-02-10 *** empty log message ***
2003-02-10 ballarin 2003-02-10 New development of algebra: Groups.
2003-02-08 paulson 2003-02-08 converting HOL/UNITY to use unconditional fairness
2003-02-08 nipkow 2003-02-08 adjusted dom rules
2003-02-07 nipkow 2003-02-07 (*f -> ( *f because of new comments
2003-02-07 nipkow 2003-02-07 Removed (*) because of comments
2003-02-07 nipkow 2003-02-07 Added (* ... *) comments in formulae.
2003-02-06 paulson 2003-02-06 changed ** to ## to avoid conflict with new comment syntax
2003-02-05 paulson 2003-02-05 more tidying
2003-02-04 paulson 2003-02-04 some x-symbols
2003-02-03 berghofe 2003-02-03 New tool for displaying version information.
2003-02-03 berghofe 2003-02-03 Fill in version information in lib/Tools/version.
2003-02-03 berghofe 2003-02-03 Added "print_intros" command.
2003-02-03 berghofe 2003-02-03 Moved print_intros from proof_general.ML to Isar/isar_cmd.ML
2003-02-03 berghofe 2003-02-03 Moved find_intros_goal from goals.ML to pure_thy.ML
2003-02-03 berghofe 2003-02-03 Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
2003-01-31 paulson 2003-01-31 conversion to new-style theories and tidying
2003-01-30 paulson 2003-01-30 conversion of UNITY theories to new-style
2003-01-30 paulson 2003-01-30 converting more UNITY theories to new-style
2003-01-29 berghofe 2003-01-29 Some tuning: - finite now uses rev_append (tail recursive!) to append stopper, because @ needs to much stack space for large strings - repeat is now tail recursive
2003-01-29 berghofe 2003-01-29 Added function rev_append.
2003-01-29 berghofe 2003-01-29 Fixed bug in function corr.