summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sun, 22 Jul 2001 21:30:21 +0200 | |

changeset 11439 | 9aaab1a160a5 |

parent 11438 | 3d9222b80989 |

child 11440 | e389e4338604 |

tuned;

--- 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 \<in> range f ==> f (myinv f y) = y"