1994-12-23 lcp 1994-12-23 csquare_rel_def: renamed k to K
1994-12-23 lcp 1994-12-23 inj_apply_equality: new
1994-12-23 lcp 1994-12-23 Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
1994-12-23 lcp 1994-12-23 empty_fun: generalized from -> to Pi
1994-12-23 lcp 1994-12-23 Changed succ(1) to 2 in cmult_2; Simplified proof of InfCard_is_Limit
1994-12-23 lcp 1994-12-23 Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type Renamed doubleton_iff to doubleton_eq_iff
1994-12-23 lcp 1994-12-23 Added Krzysztof's theorem disj_imp_disj
1994-12-21 lcp 1994-12-21 Id: marker.
1994-12-21 lcp 1994-12-21 Added comments and Id: marker.
1994-12-21 lcp 1994-12-21 Added comments and Id: marker.
1994-12-21 lcp 1994-12-21 Tools description, largely taken from ../README
1994-12-21 lcp 1994-12-21 Moved description of tools to Tools/README
1994-12-20 lcp 1994-12-20 ord_iso_rvimage: new
1994-12-20 lcp 1994-12-20 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 clasohm 1994-12-20 qed is a utility that makes ML files store the defined theories in Isabelle's theorem database
1994-12-20 lcp 1994-12-20 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 lcp 1994-12-20 Used bind_thm to store domain_rel_subset and range_rel_subset
1994-12-19 lcp 1994-12-19 removed quotes around "Datatype", and removed needless mention of [Q]Univ
1994-12-19 lcp 1994-12-19 removed quotes around "Inductive"
1994-12-19 lcp 1994-12-19 ran expandshort script
1994-12-19 lcp 1994-12-19 ran expandshort script
1994-12-19 lcp 1994-12-19 removed quotes around "Inductive"
1994-12-19 lcp 1994-12-19 added true theory dependencies
1994-12-19 lcp 1994-12-19 ran expandshort script
1994-12-16 lcp 1994-12-16 changed useless "qed" calls for lemmas back to uses of "result", and/or used "bind_thm" to declare the real results.
1994-12-16 lcp 1994-12-16 Defines ZF theory sections (inductive, datatype) at the start/ Moved theory section code here from Inductive.ML and Datatype.ML
1994-12-16 lcp 1994-12-16 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 lcp 1994-12-16 Limit_csucc: moved to InfDatatype and proved explicitly in theory InfDatatype.thy
1994-12-16 lcp 1994-12-16 put quotation marks around constant "and" because it is a keyword for inductive definitions!!
1994-12-16 lcp 1994-12-16 added thy_syntax.ML
1994-12-16 lcp 1994-12-16 Defines ZF theory sections (inductive, datatype) at the start/ Moved theory section code here from Inductive.ML and Datatype.ML
1994-12-16 lcp 1994-12-16 now also depends upon Finite.thy
1994-12-16 lcp 1994-12-16 converse_converse, converse_prod: renamed from converse_of_converse, converse_of_prod
1994-12-16 lcp 1994-12-16 moved congruence rule conj_cong2 to FOL/IFOL.ML
1994-12-16 lcp 1994-12-16 conj_cong2: new congruence rule
1994-12-15 lcp 1994-12-15 case_ss: now built upon ZF/Order/bij_inverse_ss. Deleted own bij_inverse_ss and replaces uses by case_ss
1994-12-15 lcp 1994-12-15 updated comment; renamed converse_of_Un to converse_Un
1994-12-15 lcp 1994-12-15 qconverse_qconverse, qconverse_prod: renamed from qconverse_of_qconverse, qconverse_of_prod
1994-12-14 lcp 1994-12-14 well_ord_iso_predE replaces not_well_ord_iso_pred well_ord_iso_unique: eliminated a premise using well_ord_ord_iso Proved well_ord_iso_pred_eq, ord_iso_image_pred, ord_iso_restrict_pred, part_ord_ord_iso, linear_ord_iso, wf_on_ord_iso, well_ord_ord_iso, well_ord_iso_preserving, mono_map_is_fun, mono_map_is_inj, mono_map_trans, mono_ord_isoI, well_ord_mono_ord_isoI, ord_iso_is_mono_map, ord_iso_map_mono_map, ord_iso_map_ord_iso, domain_ord_iso_map_subset, domain_ord_iso_map_cases, range_ord_iso_map_cases, well_ord_trichotomy deleted bij_ss in favour of bij_inverse_ss
1994-12-14 lcp 1994-12-14 Ord_iso_implies_eq_lemma: uses well_ord_iso_predE instead of not_well_ord_iso_pred
1994-12-14 lcp 1994-12-14 converse_UN, Diff_eq_0_iff: new
1994-12-14 lcp 1994-12-14 added constants mono_map, ord_iso_map
1994-12-14 lcp 1994-12-14 cardinal_UN_Ord_lt_csucc: added comment le_UN_Ord_lt_csucc: tided proof by proving the lemma inj_UN_subset
1994-12-14 lcp 1994-12-14 conj_commute,disj_commute: new
1994-12-14 clasohm 1994-12-14 changed get_thm to search all parent theories if the theorem is not found in the current theory
1994-12-14 clasohm 1994-12-14 added bind_thm for theorems defined by "standard ..."
1994-12-14 wenzelm 1994-12-14 added any, sprop to pure_types;
1994-12-14 wenzelm 1994-12-14 removed "logic1"; improved typ_to_nonterm;
1994-12-13 clasohm 1994-12-13 removed FOL_Lemmas and IFOL_Lemmas; added qed_goal
1994-12-12 wenzelm 1994-12-12 added print_theory that prints stored thms;
1994-12-09 wenzelm 1994-12-09 minor internal changes;
1994-12-09 wenzelm 1994-12-09 improved axioms_of: returns thms as the manual says;
1994-12-09 clasohm 1994-12-09 removed ZF_Lemmas and added qed_goal
1994-12-09 clasohm 1994-12-09 added warning for already stored theorem to store_thm
1994-12-08 lcp 1994-12-08 sum_ss: moved down and added the rewrite rules for "case"
1994-12-08 lcp 1994-12-08 leI: added comment
1994-12-08 lcp 1994-12-08 lt_eq_pred, Ord_iso_implies_eq: new, for Kunens Theorem 7.3
1994-12-08 lcp 1994-12-08 sum_ss: deleted because it conflicts with the one in Sum.ML
1994-12-08 lcp 1994-12-08 not_well_ord_iso_pred: removed needless quantifier
1994-12-08 lcp 1994-12-08 UN_upper_cardinal: updated to refer to Card_le_imp_lepoll and lepoll_imp_Card_le