summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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"