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