src/HOL/Inductive.thy
changeset 11439 9aaab1a160a5
parent 11436 3f74b80d979f
child 11688 56833637db2a
     1.1 --- a/src/HOL/Inductive.thy	Sun Jul 22 21:30:05 2001 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Sun Jul 22 21:30:21 2001 +0200
     1.3 @@ -68,7 +68,7 @@
     1.4    hence "(THE x'. f x' = f x) = (THE x'. x' = x)"
     1.5      by (simp only: inj_eq)
     1.6    also have "... = x" by (rule the_eq_trivial)
     1.7 -  finally (trans) show ?thesis by (unfold myinv_def)
     1.8 +  finally show ?thesis by (unfold myinv_def)
     1.9  qed
    1.10  
    1.11  lemma f_myinv_f: "inj f ==> y \<in> range f ==> f (myinv f y) = y"