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.
Modified proofs for new claset primitives. The problem is that they enforce
authorlcp
Fri, 28 Apr 1995 11:41:59 +0200
changeset 1076 68f088887f48
parent 1075 848bf2e18dff
child 1077 c2df11ae8b55
Modified proofs for new claset primitives. The problem is that they enforce the "most recent added rule has priority" policy more strictly now.
src/ZF/EquivClass.ML file | annotate | diff | comparison | revisions 
--- a/src/ZF/EquivClass.ML	Fri Apr 28 11:31:33 1995 +0200
+++ b/src/ZF/EquivClass.ML	Fri Apr 28 11:41:59 1995 +0200
@@ -79,7 +79,7 @@
 qed "equiv_class_nondisjoint";
 
 goalw EquivClass.thy [equiv_def] "!!A r. equiv(A,r) ==> r <= A*A";
-by (safe_tac ZF_cs);
+by (safe_tac subset_cs);
 qed "equiv_type";
 
 goal EquivClass.thy
isabelle