src/ZF/ex/misc.ML
Mon, 02 Feb 1998 12:57:20 +0100 paulson New example, Pow_Sigma_bij
Wed, 24 Dec 1997 10:02:30 +0100 paulson New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
Fri, 28 Nov 1997 10:36:08 +0100 paulson New example
Wed, 05 Nov 1997 13:14:15 +0100 paulson Ran expandshort, especially to introduce Safe_tac
Tue, 04 Nov 1997 09:26:15 +0100 wenzelm isatool fixclasimp;
Mon, 03 Nov 1997 12:24:13 +0100 wenzelm isatool fixclasimp;
Mon, 21 Apr 1997 10:16:41 +0200 paulson Moved blast_tac demo from ZF/func.ML to ZF/ex/misc.ML
Thu, 09 Jan 1997 10:20:03 +0100 paulson Removal of needless "addIs [equality]", etc.
Fri, 03 Jan 1997 15:01:55 +0100 paulson Implicit simpsets and clasets for FOL and ZF
Mon, 03 Jun 1996 11:41:00 +0200 paulson Shortened a proof
Thu, 04 Apr 1996 15:34:52 +0200 paulson updated comments
Tue, 30 Jan 1996 13:42:57 +0100 clasohm expanded tabs
Thu, 04 May 1995 02:02:54 +0200 lcp Changed some definitions and proofs to use pattern-matching.
Wed, 14 Dec 1994 11:41:49 +0100 clasohm added bind_thm for theorems defined by "standard ..."
Thu, 24 Nov 1994 00:33:13 +0100 lcp moved Cantors theorem to ZF/ZF.ML and ZF/Perm.ML
Thu, 03 Nov 1994 16:39:41 +0100 lcp ZF/ex/Ramsey,Rmap,misc.ML: modified for new definition of Pi(A,B)
Tue, 21 Jun 1994 16:26:34 +0200 lcp Various updates and tidying
Thu, 07 Oct 1993 11:47:50 +0100 lcp used ~: for "not in"
Thu, 30 Sep 1993 10:54:01 +0100 lcp ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
Fri, 17 Sep 1993 16:52:10 +0200 lcp Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
Thu, 16 Sep 1993 12:20:38 +0200 clasohm Initial revision
less more (0) tip