src/HOL/MiniML/Type.ML
1999-01-09 nipkow Refined arith tactic.
1998-11-27 nipkow At last: linear arithmetic for nat!
1998-09-21 oheimb re-added mem and list_all
1998-09-09 oheimb reflecting changes to Option.ML, List.{thy|ML}, mainly list_all
1998-07-24 berghofe Adapted to new datatype package.
1998-07-03 nipkow Removed leading !! in goals.
1998-06-22 wenzelm isatool fixgoal;
1998-03-07 nipkow Removed `addsplits [expand_if]'
1997-12-30 nipkow nth -> !
1997-11-05 paulson Ran expandshort, especially to introduce Safe_tac
1997-11-03 wenzelm isatool fixclasimp;
1997-10-17 nipkow setloop split_tac -> addsplits
1997-10-16 nipkow Simplified proof because of better simplifier.
1997-10-10 wenzelm fixed dots;
1997-06-16 paulson Type constraint added to ensure that "length" refers to lists. Maybe should
1997-06-02 paulson New statement and proof of free_tv_subst_var in order to cope with new
1997-04-23 paulson Ran expandshort
1997-04-22 paulson Ran expandshort
1997-02-14 narasche Some lemmas changed to valuesd
1997-01-17 nipkow The new version of MiniML including "let".
1997-01-17 paulson New miniscoping rules for the bounded quantifiers and UN/INT operators
1996-09-26 paulson Ran expandshort
1996-08-08 berghofe Removed unnecessary Addsimps.
1996-05-20 nipkow Added thm I_complete_wrt_W to I.
1996-03-27 paulson Now use _irrefl instead of _anti_refl
1996-02-27 nipkow used qed_spec_mp.
1996-01-30 clasohm expanded tabs
1995-12-08 nipkow Introduced Monad syntax Pat := Val; Cont
1995-10-25 nipkow New theory: type inference for let-free MiniML
less more (0) tip