src/HOL/MiniML/Type.ML
2004-02-19 paulson 2004-02-19 removal of the legacy ML structure List
2002-10-08 nipkow 2002-10-08 Got rid of rotates because of new simplifier
2000-08-30 nipkow 2000-08-30 introduced induct_thm_tac
1999-01-09 nipkow 1999-01-09 Refined arith tactic.
1998-11-27 nipkow 1998-11-27 At last: linear arithmetic for nat!
1998-09-21 oheimb 1998-09-21 re-added mem and list_all
1998-09-09 oheimb 1998-09-09 reflecting changes to Option.ML, List.{thy|ML}, mainly list_all
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1998-07-03 nipkow 1998-07-03 Removed leading !! in goals.
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1998-03-07 nipkow 1998-03-07 Removed `addsplits [expand_if]'
1997-12-30 nipkow 1997-12-30 nth -> !
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