Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Ord_iso_implies_eq_lemma: uses well_ord_iso_predE instead of
authorlcp
Wed, 14 Dec 1994 17:15:54 +0100
changeset 788 8acbe6f3de2b
parent 787 1affbb1c5f1f
child 789 30bdc59198ff
Ord_iso_implies_eq_lemma: uses well_ord_iso_predE instead of not_well_ord_iso_pred
src/ZF/OrderType.ML file | annotate | diff | comparison | revisions 
--- a/src/ZF/OrderType.ML	Wed Dec 14 16:57:55 1994 +0100
+++ b/src/ZF/OrderType.ML	Wed Dec 14 17:15:54 1994 +0100
@@ -231,8 +231,8 @@
 \         |] ==> R";
 by (forward_tac [lt_eq_pred] 1);
 be ltE 1;
-by (rtac (well_ord_Memrel RS not_well_ord_iso_pred RS notE) 1 THEN
-    assume_tac 1 THEN assume_tac 1);
+by (rtac (well_ord_Memrel RS well_ord_iso_predE) 1 THEN
+    assume_tac 3 THEN assume_tac 1);
 be subst 1;
 by (asm_full_simp_tac (ZF_ss addsimps [ord_iso_def]) 1);
 (*Combining the two simplifications causes looping*)
isabelle