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

author | wenzelm |

Wed, 07 Feb 2001 20:57:03 +0100 | |

changeset 11083 | d8fda557e476 |

parent 11082 | 9a7cdfaa7ecb |

child 11084 | 32c1deea5bcd |

tuned;

--- a/src/HOL/subset.thy Wed Feb 07 20:56:40 2001 +0100 +++ b/src/HOL/subset.thy Wed Feb 07 20:57:03 2001 +0100 @@ -66,8 +66,8 @@ proof assume "Abs x = Abs y" hence "Rep (Abs x) = Rep (Abs y)" by simp - moreover note x hence "Rep (Abs x) = x" by (rule Abs_inverse [OF tydef]) - moreover note y hence "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef]) + moreover from x have "Rep (Abs x) = x" by (rule Abs_inverse [OF tydef]) + moreover from y have "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef]) ultimately show "x = y" by (simp only:) next assume "x = y"