# HG changeset patch
# User wenzelm
# Date 995830221 -7200
# Node ID 9aaab1a160a51df67089633da8bdc4869f56be47
# Parent 3d9222b8098998617045df06e9788034095bb8b5
tuned;
diff -r 3d9222b80989 -r 9aaab1a160a5 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy Sun Jul 22 21:30:05 2001 +0200
+++ b/src/HOL/Inductive.thy Sun Jul 22 21:30:21 2001 +0200
@@ -68,7 +68,7 @@
hence "(THE x'. f x' = f x) = (THE x'. x' = x)"
by (simp only: inj_eq)
also have "... = x" by (rule the_eq_trivial)
- finally (trans) show ?thesis by (unfold myinv_def)
+ finally show ?thesis by (unfold myinv_def)
qed
lemma f_myinv_f: "inj f ==> y \ range f ==> f (myinv f y) = y"