src/HOL/MiniML/Type.ML
1997-11-05 paulson 1997-11-05 Ran expandshort, especially to introduce Safe_tac
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-10-17 nipkow 1997-10-17 setloop split_tac -> addsplits
1997-10-16 nipkow 1997-10-16 Simplified proof because of better simplifier.
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-06-16 paulson 1997-06-16 Type constraint added to ensure that "length" refers to lists. Maybe should not be needed, but the translation length->size happens irrespective of types
1997-06-02 paulson 1997-06-02 New statement and proof of free_tv_subst_var in order to cope with new rewrite rules Un_insert_left, Un_insert_right
1997-04-23 paulson 1997-04-23 Ran expandshort
1997-04-22 paulson 1997-04-22 Ran expandshort
1997-02-14 narasche 1997-02-14 Some lemmas changed to valuesd
1997-01-17 nipkow 1997-01-17 The new version of MiniML including "let".
1997-01-17 paulson 1997-01-17 New miniscoping rules for the bounded quantifiers and UN/INT operators
1996-09-26 paulson 1996-09-26 Ran expandshort
1996-08-08 berghofe 1996-08-08 Removed unnecessary Addsimps.
1996-05-20 nipkow 1996-05-20 Added thm I_complete_wrt_W to I. Added a few lemmas to Maybe and Type.
1996-03-27 paulson 1996-03-27 Now use _irrefl instead of _anti_refl
1996-02-27 nipkow 1996-02-27 used qed_spec_mp.
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-12-08 nipkow 1995-12-08 Introduced Monad syntax Pat := Val; Cont
1995-10-25 nipkow 1995-10-25 New theory: type inference for let-free MiniML