1994-12-23 Changed succ(1) to 2 in in_VLimit, two_in_univ
lcp [Fri, 23 Dec 1994 16:29:53 +0100] rev 828
Changed succ(1) to 2 in in_VLimit, two_in_univ
1994-12-23 csquare_rel_def: renamed k to K
lcp [Fri, 23 Dec 1994 16:29:04 +0100] rev 827
csquare_rel_def: renamed k to K
1994-12-23 inj_apply_equality: new
lcp [Fri, 23 Dec 1994 16:28:26 +0100] rev 826
inj_apply_equality: new
1994-12-23 Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp [Fri, 23 Dec 1994 16:27:45 +0100] rev 825
Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
1994-12-23 empty_fun: generalized from -> to Pi
lcp [Fri, 23 Dec 1994 16:27:07 +0100] rev 824
empty_fun: generalized from -> to Pi
1994-12-23 Changed succ(1) to 2 in cmult_2; Simplified proof of InfCard_is_Limit
lcp [Fri, 23 Dec 1994 16:26:34 +0100] rev 823
Changed succ(1) to 2 in cmult_2; Simplified proof of InfCard_is_Limit
1994-12-23 Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
lcp [Fri, 23 Dec 1994 16:25:45 +0100] rev 822
Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type Renamed doubleton_iff to doubleton_eq_iff
1994-12-23 Added Krzysztof's theorem disj_imp_disj
lcp [Fri, 23 Dec 1994 10:52:25 +0100] rev 821
Added Krzysztof's theorem disj_imp_disj
1994-12-21 Id: marker.
lcp [Wed, 21 Dec 1994 13:36:02 +0100] rev 820
Id: marker.
1994-12-21 Added comments and Id: marker.
lcp [Wed, 21 Dec 1994 13:26:26 +0100] rev 819
Added comments and Id: marker.
1994-12-21 Added comments and Id: marker.
lcp [Wed, 21 Dec 1994 13:10:39 +0100] rev 818
Added comments and Id: marker.
1994-12-21 Tools description, largely taken from ../README
lcp [Wed, 21 Dec 1994 12:53:45 +0100] rev 817
Tools description, largely taken from ../README
1994-12-21 Moved description of tools to Tools/README
lcp [Wed, 21 Dec 1994 12:46:52 +0100] rev 816
Moved description of tools to Tools/README
1994-12-20 ord_iso_rvimage: new
lcp [Tue, 20 Dec 1994 16:20:50 +0100] rev 815
ord_iso_rvimage: new
1994-12-20 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp [Tue, 20 Dec 1994 15:58:52 +0100] rev 814
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, Ord_iso_implies_eq to top of file, as they do not require the other material. Simplified proof of ordertype_subset. Proved ordertype_eq: a short proof using deepen_tac! Deleted bij_ordermap_vimage and ordermap_Memrel "bij_ordermap_vimage and ordermap_Memrelf. [| f: bij(A,B); well_ord(B,r); x:A |] ==>\ \ ordermap(A,rvimage(A,f,r)) ` x = ordermap(B,r) ` (f`x)"; "\ ordermap(A,rvimage(A,f,r)) ` x = ordermap(B,r) ` (f`x)";i. [| Ord(i); j:i |] ==> ordermap(i,Memrel(i)) ` j = j" because ordertype_eq serves the same purpose. Proofs of bij_ordertype_vimage and ordertype_Memrel are now trivial.
1994-12-20 qed is a utility that makes ML files store the defined theories in Isabelle's
clasohm [Tue, 20 Dec 1994 13:24:04 +0100] rev 813
qed is a utility that makes ML files store the defined theories in Isabelle's theorem database
1994-12-20 Simplified proof of ord_iso_image_pred using bij_inverse_ss.
lcp [Tue, 20 Dec 1994 10:21:32 +0100] rev 812
Simplified proof of ord_iso_image_pred using bij_inverse_ss. Replaced not_well_ord_iso_pred_lemma by much simpler well_ord_iso_subset_lemma. Simplifed proof of well_ord_iso_unique_lemma using well_ord_iso_subset_lemma.
1994-12-20 Used bind_thm to store domain_rel_subset and range_rel_subset
lcp [Tue, 20 Dec 1994 10:19:24 +0100] rev 811
Used bind_thm to store domain_rel_subset and range_rel_subset
1994-12-19 removed quotes around "Datatype",
lcp [Mon, 19 Dec 1994 15:30:30 +0100] rev 810
removed quotes around "Datatype", and removed needless mention of [Q]Univ
1994-12-19 removed quotes around "Inductive"
lcp [Mon, 19 Dec 1994 15:22:42 +0100] rev 809
removed quotes around "Inductive"
1994-12-19 ran expandshort script
lcp [Mon, 19 Dec 1994 15:17:29 +0100] rev 808
ran expandshort script
1994-12-19 ran expandshort script
lcp [Mon, 19 Dec 1994 15:11:50 +0100] rev 807
ran expandshort script
1994-12-19 removed quotes around "Inductive"
lcp [Mon, 19 Dec 1994 13:24:58 +0100] rev 806
removed quotes around "Inductive"
1994-12-19 added true theory dependencies
lcp [Mon, 19 Dec 1994 13:18:54 +0100] rev 805
added true theory dependencies
1994-12-19 ran expandshort script
lcp [Mon, 19 Dec 1994 13:01:30 +0100] rev 804
ran expandshort script
1994-12-16 changed useless "qed" calls for lemmas back to uses of "result",
lcp [Fri, 16 Dec 1994 18:07:12 +0100] rev 803
changed useless "qed" calls for lemmas back to uses of "result", and/or used "bind_thm" to declare the real results.
1994-12-16 Defines ZF theory sections (inductive, datatype) at the start/
lcp [Fri, 16 Dec 1994 17:46:02 +0100] rev 802
Defines ZF theory sections (inductive, datatype) at the start/ Moved theory section code here from Inductive.ML and Datatype.ML
1994-12-16 Added Limit_csucc from CardinalArith
lcp [Fri, 16 Dec 1994 17:44:09 +0100] rev 801
Added Limit_csucc from CardinalArith Moved all theorems concerning FINITE functions to Univ.ML and deleted the declaration val Fin_Univ_thy = merge_theories (Univ.thy,Finite.thy);
1994-12-16 Limit_csucc: moved to InfDatatype and proved explicitly in
lcp [Fri, 16 Dec 1994 17:41:49 +0100] rev 800
Limit_csucc: moved to InfDatatype and proved explicitly in theory InfDatatype.thy
1994-12-16 put quotation marks around constant "and" because it is a
lcp [Fri, 16 Dec 1994 17:39:43 +0100] rev 799
put quotation marks around constant "and" because it is a keyword for inductive definitions!!
(0) -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip