1996-04-19 clasohm 1996-04-19 added Konrad's code for the datatype package
1996-04-19 clasohm 1996-04-19 adapted to new version of Fun.ML
1996-04-19 clasohm 1996-04-19 removed assignment of HOL_ss to simpset
1996-04-19 clasohm 1996-04-19 added thy_data.ML
1996-04-19 clasohm 1996-04-19 added thyname_of_sign (used in HOL/thy_data.ML)
1996-04-18 oheimb 1996-04-18 adapted proof of drop_succ_Cons: problem with non-confluent simpset removed
1996-04-18 oheimb 1996-04-18 adapted proof of less_succ: problem because of non-confluent SimpSet removed
1996-04-18 oheimb 1996-04-18 *** empty log message ***
1996-04-17 oheimb 1996-04-17 *** empty log message ***
1996-04-17 oheimb 1996-04-17 *** empty log message ***
1996-04-12 clasohm 1996-04-12 add_thydata and get_thydata now take a string as their first argument
1996-04-12 clasohm 1996-04-12 changed first parameter of add_thydata and get_thydata
1996-04-11 clasohm 1996-04-11 fixed bug in set_current_thy
1996-04-11 nipkow 1996-04-11 Added a number of lemmas
1996-04-09 berghofe 1996-04-09 select_match now sorts list of matching theorems according to the number of premises and size of the required substitution
1996-04-04 nipkow 1996-04-04 Replaced !simpset by HOL_ss on line 93.
1996-04-04 paulson 1996-04-04 Proved Inter_0 and converse_INT
1996-04-04 paulson 1996-04-04 deleted obsolete comment
1996-04-04 nipkow 1996-04-04 Added 'constdefs'
1996-04-04 nipkow 1996-04-04 Added 'constdefs' and extended the section on 'defs'
1996-04-04 nipkow 1996-04-04 Messed up last update.
1996-04-04 nipkow 1996-04-04 Replaced \CHOL by \HOLCF
1996-04-04 paulson 1996-04-04 updated comments
1996-04-04 nipkow 1996-04-04 Moved link to paper.
1996-04-04 oheimb 1996-04-04 Removed 8bit characters used by mistake
1996-04-04 paulson 1996-04-04 Fixed error in CHANGED (caused by variable renaming)
1996-04-04 paulson 1996-04-04 Using new "Times" infix
1996-04-04 paulson 1996-04-04 For renaming to rtrancl_Un_rtrancl
1996-04-04 paulson 1996-04-04 Added more _iff rewrites for Compl, Un, Int
1996-04-04 paulson 1996-04-04 New example Comb: Church-Rosser for combinators, ported from ZF
1996-04-03 oheimb 1996-04-03 *** empty log message ***
1996-04-03 oheimb 1996-04-03 Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
1996-04-03 nipkow 1996-04-03 Introduced Times and SIGMA.
1996-04-03 oheimb 1996-04-03 *** empty log message ***
1996-04-03 nipkow 1996-04-03 Plugged some more loopholes with nodup_Vars.
1996-03-29 paulson 1996-03-29 Simplified proof of tiling_UnI
1996-03-29 paulson 1996-03-29 Binary integers and their numeric syntax
1996-03-29 paulson 1996-03-29 new lemma for mutilated chess board
1996-03-29 paulson 1996-03-29 Simplified proof of tiling_UnI
1996-03-29 paulson 1996-03-29 Mended indentation
1996-03-28 berghofe 1996-03-28 Added functions pr_latex and printgoal_latex which display current proof state in xdvi window
1996-03-28 berghofe 1996-03-28 Optimized type inference (avoids chains of the form 'a |-> 'b |-> 'c ... in tye)
1996-03-28 paulson 1996-03-28 Moved even/odd lemmas from ex/Mutil to Arith
1996-03-28 paulson 1996-03-28 Translations for 1 and 2 moved from Hoare/Examples.thy to Nat.thy
1996-03-28 paulson 1996-03-28 Alternative proof removes dependence upon AC
1996-03-28 paulson 1996-03-28 Ran expandshort
1996-03-28 paulson 1996-03-28 New theorem Finite_imp_succ_cardinal_Diff
1996-03-27 paulson 1996-03-27 New mutilated checkerboard example
1996-03-27 paulson 1996-03-27 Added Mutil to ex targets
1996-03-27 paulson 1996-03-27 Now use _irrefl instead of _anti_refl
1996-03-27 paulson 1996-03-27 Library changes for mutilated checkerboard
1996-03-26 paulson 1996-03-26 Simplified proofs, esp. for new ZF_ss
1996-03-26 paulson 1996-03-26 Moved some proofs to Cardinal.ML; simplified others
1996-03-26 paulson 1996-03-26 Moved some proofs to FOL/IFOL.ML
1996-03-26 paulson 1996-03-26 Rewriting changes due to new arith_ss
1996-03-26 paulson 1996-03-26 Now loads Mutil example
1996-03-26 paulson 1996-03-26 Added new rewrite rules about cons and succ
1996-03-26 paulson 1996-03-26 New results from AC/Cardinal_aux.ML
1996-03-26 paulson 1996-03-26 Updated comments
1996-03-26 paulson 1996-03-26 New lemmas for Mutilated Checkerboard