src/ZF/Univ.ML
Fri, 12 Dec 1997 10:46:09 +0100 paulson new blast_tac no longer works here
Wed, 05 Nov 1997 13:14:15 +0100 paulson Ran expandshort, especially to introduce Safe_tac
Mon, 03 Nov 1997 12:24:13 +0100 wenzelm isatool fixclasimp;
Thu, 16 Oct 1997 13:39:20 +0200 wenzelm moved rank_Inl, rank_Inr from Epsilon.ML to Univ.ML;
Mon, 29 Sep 1997 11:56:04 +0200 paulson Much tidying including step_tac -> clarify_tac or safe_tac; sometimes
Wed, 30 Apr 1997 11:42:37 +0200 paulson New theorems Pow_in_Vfrom and Pow_in_VLimit
Wed, 23 Apr 1997 10:54:22 +0200 paulson Conversion to use blast_tac
Wed, 09 Apr 1997 12:37:44 +0200 paulson Using Blast_tac
Wed, 08 Jan 1997 15:04:27 +0100 paulson Removal of sum_cs and eq_cs
Fri, 03 Jan 1997 15:01:55 +0100 paulson Implicit simpsets and clasets for FOL and ZF
Thu, 26 Sep 1996 15:14:23 +0200 paulson Ran expandshort; used stac instead of ssubst
Tue, 30 Jan 1996 13:42:57 +0100 clasohm expanded tabs
Thu, 12 Jan 1995 03:02:05 +0100 lcp Moved theorems Ord_cases_lemma and Ord_cases to Ordinal.ML
Fri, 23 Dec 1994 16:29:53 +0100 lcp Changed succ(1) to 2 in in_VLimit, two_in_univ
Fri, 16 Dec 1994 18:07:12 +0100 lcp changed useless "qed" calls for lemmas back to uses of "result",
Wed, 14 Dec 1994 11:41:49 +0100 clasohm added bind_thm for theorems defined by "standard ..."
Wed, 07 Dec 1994 13:12:04 +0100 clasohm added qed and qed_goal[w]
Wed, 17 Aug 1994 10:31:35 +0200 lcp ZF/Univ/Sigma_subset_univ, Transset_Pair_subset_univ: deleted
Fri, 12 Aug 1994 12:51:34 +0200 lcp installation of new inductive/datatype sections
Wed, 27 Jul 1994 15:33:42 +0200 lcp Addition of infinite branching datatypes
Tue, 26 Jul 1994 13:21:20 +0200 lcp Axiom of choice, cardinality results, etc.
Tue, 21 Jun 1994 17:20:34 +0200 lcp Addition of cardinals and order types, various tidying
Mon, 06 Dec 1993 10:57:22 +0100 lcp ZF/univ/in_Vfrom_limit: new
Thu, 07 Oct 1993 10:48:16 +0100 lcp added ~: for "not in"
Tue, 05 Oct 1993 17:15:28 +0100 lcp Retry of the previous commit (network outage)
Thu, 30 Sep 1993 10:26:38 +0100 lcp ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
Fri, 17 Sep 1993 16:16:38 +0200 lcp Installation of new simplifier for ZF. Deleted all congruence rules not
Thu, 16 Sep 1993 12:20:38 +0200 clasohm Initial revision
less more (0) tip