Wed, 21 Dec 1994 12:53:45 +0100 Tools description, largely taken from ../README
lcp [Wed, 21 Dec 1994 12:53:45 +0100] rev 817
Tools description, largely taken from ../README
Wed, 21 Dec 1994 12:46:52 +0100 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
Tue, 20 Dec 1994 16:20:50 +0100 ord_iso_rvimage: new
lcp [Tue, 20 Dec 1994 16:20:50 +0100] rev 815
ord_iso_rvimage: new
Tue, 20 Dec 1994 15:58:52 +0100 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.
Tue, 20 Dec 1994 13:24:04 +0100 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
Tue, 20 Dec 1994 10:21:32 +0100 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.
Tue, 20 Dec 1994 10:19:24 +0100 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
Mon, 19 Dec 1994 15:30:30 +0100 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
Mon, 19 Dec 1994 15:22:42 +0100 removed quotes around "Inductive"
lcp [Mon, 19 Dec 1994 15:22:42 +0100] rev 809
removed quotes around "Inductive"
Mon, 19 Dec 1994 15:17:29 +0100 ran expandshort script
lcp [Mon, 19 Dec 1994 15:17:29 +0100] rev 808
ran expandshort script
(0) -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip