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.
qconverse_qconverse, qconverse_prod: renamed from
authorlcp
Thu, 15 Dec 1994 11:08:22 +0100
changeset 790 4c10e8532d43
parent 789 30bdc59198ff
child 791 354a56e923ff
qconverse_qconverse, qconverse_prod: renamed from qconverse_of_qconverse, qconverse_of_prod
src/ZF/QPair.ML file | annotate | diff | comparison | revisions 
--- a/src/ZF/QPair.ML	Wed Dec 14 17:24:23 1994 +0100
+++ b/src/ZF/QPair.ML	Thu Dec 15 11:08:22 1994 +0100
@@ -125,7 +125,7 @@
 val qconverse_cs = qpair_cs addSIs [qconverseI] 
 			    addSEs [qconverseD,qconverseE];
 
-qed_goal "qconverse_of_qconverse" QPair.thy
+qed_goal "qconverse_qconverse" QPair.thy
     "!!A B r. r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r"
  (fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]);
 
@@ -133,7 +133,7 @@
     "!!A B r. r <= A <*> B ==> qconverse(r) <= B <*> A"
  (fn _ => [ (fast_tac qconverse_cs 1) ]);
 
-qed_goal "qconverse_of_prod" QPair.thy "qconverse(A <*> B) = B <*> A"
+qed_goal "qconverse_prod" QPair.thy "qconverse(A <*> B) = B <*> A"
  (fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]);
 
 qed_goal "qconverse_empty" QPair.thy "qconverse(0) = 0"
isabelle