lcp [Fri, 23 Dec 1994 16:34:27 +0100] rev 834
singleton_iff: new
lcp [Fri, 23 Dec 1994 16:33:37 +0100] rev 833
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
succ_eqpoll_succD, cons_lepoll_cons_iff, cons_eqpoll_cons_iff. Deleted
inj_succ_succD. Streamlined proof of nat_lepoll_imp_le_lemma. Added
Krzysztof's theorems diff_sing_lepoll, lepoll_diff_sing, diff_sing_eqpoll,
lepoll_1_is_sing, inj_not_surj_succ, lesspoll_trans, lesspoll_lepoll_lesspoll,
lepoll_lesspoll_lesspoll, lepoll_imp_lesspoll_succ, lesspoll_succ_imp_lepoll,
lepoll_succ_disj, lepoll_nat_imp_Finite, lepoll_Finite,
Finite_imp_cons_Finite, Finite_imp_succ_Finite, nat_le_infinite_Ord,
nat_wf_on_converse_Memrel, nat_well_ord_converse_Memrel, well_ord_converse,
ordertype_eq_n, Finite_well_ord_converse
lcp [Fri, 23 Dec 1994 16:32:39 +0100] rev 832
Added Krzysztof's constants lesspoll and Finite
lcp [Fri, 23 Dec 1994 16:32:02 +0100] rev 831
Added Krzysztof's theorem pred_Memrel
lcp [Fri, 23 Dec 1994 16:31:23 +0100] rev 830
Moved Transset_includes_summands and Transset_sum_Int_subset to
QUniv.thy to eliminate use of merge_theories. Proved Memrel_type.
Added Krzysztof's theorems Memrel_mono, Memrel_empty, lt_Ord, succ_le_imp_le
lcp [Fri, 23 Dec 1994 16:30:35 +0100] rev 829
natE0: deleted, since unused
lcp [Fri, 23 Dec 1994 16:29:53 +0100] rev 828
Changed succ(1) to 2 in in_VLimit, two_in_univ
lcp [Fri, 23 Dec 1994 16:29:04 +0100] rev 827
csquare_rel_def: renamed k to K
lcp [Fri, 23 Dec 1994 16:28:26 +0100] rev 826
inj_apply_equality: new
lcp [Fri, 23 Dec 1994 16:27:45 +0100] rev 825
Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
lcp [Fri, 23 Dec 1994 16:27:07 +0100] rev 824
empty_fun: generalized from -> to Pi
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
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
lcp [Fri, 23 Dec 1994 10:52:25 +0100] rev 821
Added Krzysztof's theorem disj_imp_disj
lcp [Wed, 21 Dec 1994 13:36:02 +0100] rev 820
Id: marker.
lcp [Wed, 21 Dec 1994 13:26:26 +0100] rev 819
Added comments and Id: marker.
lcp [Wed, 21 Dec 1994 13:10:39 +0100] rev 818
Added comments and Id: marker.
lcp [Wed, 21 Dec 1994 12:53:45 +0100] rev 817
Tools description, largely taken from ../README
lcp [Wed, 21 Dec 1994 12:46:52 +0100] rev 816
Moved description of tools to Tools/README
lcp [Tue, 20 Dec 1994 16:20:50 +0100] rev 815
ord_iso_rvimage: new
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.
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
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.
lcp [Tue, 20 Dec 1994 10:19:24 +0100] rev 811
Used bind_thm to store domain_rel_subset and range_rel_subset
lcp [Mon, 19 Dec 1994 15:30:30 +0100] rev 810
removed quotes around "Datatype",
and removed needless mention of [Q]Univ
lcp [Mon, 19 Dec 1994 15:22:42 +0100] rev 809
removed quotes around "Inductive"
lcp [Mon, 19 Dec 1994 15:17:29 +0100] rev 808
ran expandshort script
lcp [Mon, 19 Dec 1994 15:11:50 +0100] rev 807
ran expandshort script
lcp [Mon, 19 Dec 1994 13:24:58 +0100] rev 806
removed quotes around "Inductive"
lcp [Mon, 19 Dec 1994 13:18:54 +0100] rev 805
added true theory dependencies