src/HOL/MiniML/Type.ML
Fri, 17 Oct 1997 15:25:12 +0200 nipkow setloop split_tac -> addsplits
Thu, 16 Oct 1997 14:12:58 +0200 nipkow Simplified proof because of better simplifier.
Fri, 10 Oct 1997 19:02:28 +0200 wenzelm fixed dots;
Mon, 16 Jun 1997 14:25:33 +0200 paulson Type constraint added to ensure that "length" refers to lists. Maybe should
Mon, 02 Jun 1997 12:15:13 +0200 paulson New statement and proof of free_tv_subst_var in order to cope with new
Wed, 23 Apr 1997 11:02:19 +0200 paulson Ran expandshort
Tue, 22 Apr 1997 11:45:22 +0200 paulson Ran expandshort
Fri, 14 Feb 1997 16:01:43 +0100 narasche Some lemmas changed to valuesd
Fri, 17 Jan 1997 18:50:04 +0100 nipkow The new version of MiniML including "let".
Fri, 17 Jan 1997 11:09:19 +0100 paulson New miniscoping rules for the bounded quantifiers and UN/INT operators
Thu, 26 Sep 1996 12:47:47 +0200 paulson Ran expandshort
Thu, 08 Aug 1996 11:45:04 +0200 berghofe Removed unnecessary Addsimps.
Mon, 20 May 1996 18:41:55 +0200 nipkow Added thm I_complete_wrt_W to I.
Wed, 27 Mar 1996 18:46:42 +0100 paulson Now use _irrefl instead of _anti_refl
Tue, 27 Feb 1996 18:22:47 +0100 nipkow used qed_spec_mp.
Tue, 30 Jan 1996 15:24:36 +0100 clasohm expanded tabs
Fri, 08 Dec 1995 19:48:15 +0100 nipkow Introduced Monad syntax Pat := Val; Cont
Wed, 25 Oct 1995 09:46:46 +0100 nipkow New theory: type inference for let-free MiniML
less more (0) tip