src/HOL/UNITY/Extend.thy
changeset 7378 ed9230a0a700
parent 7342 532841541d73
child 7399 cf780c2bcccf
     1.1 --- a/src/HOL/UNITY/Extend.thy	Fri Aug 27 15:44:27 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Extend.thy	Fri Aug 27 15:46:58 1999 +0200
     1.3 @@ -41,8 +41,7 @@
     1.4      f_act   :: "('c * 'c) set => ('a*'a) set"
     1.5  
     1.6    assumes
     1.7 -    inj_h  "inj h"
     1.8 -    surj_h "surj h"
     1.9 +    bij_h  "bij h"
    1.10    defines
    1.11      f_def       "f z == fst (inv h z)"
    1.12      g_def       "g z == snd (inv h z)"