Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/UNITY/Extend.thy
changeset 7378 ed9230a0a700
parent 7342 532841541d73
child 7399 cf780c2bcccf 
--- a/src/HOL/UNITY/Extend.thy	Fri Aug 27 15:44:27 1999 +0200
+++ b/src/HOL/UNITY/Extend.thy	Fri Aug 27 15:46:58 1999 +0200
@@ -41,8 +41,7 @@
     f_act   :: "('c * 'c) set => ('a*'a) set"
 
   assumes
-    inj_h  "inj h"
-    surj_h "surj h"
+    bij_h  "bij h"
   defines
     f_def       "f z == fst (inv h z)"
     g_def       "g z == snd (inv h z)"
isabelle