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

src/HOL/Import/HOL4Setup.thy

changeset 41550 | efa734d9b221 |

parent 34208 | a7acd6c68d9b |

child 43918 | 6ca79a354c51 |

1.1 --- a/src/HOL/Import/HOL4Setup.thy Fri Jan 14 15:43:04 2011 +0100 1.2 +++ b/src/HOL/Import/HOL4Setup.thy Fri Jan 14 15:44:47 2011 +0100 1.3 @@ -90,11 +90,11 @@ 1.4 have ed: "TYPE_DEFINITION P Rep" 1.5 proof (auto simp add: TYPE_DEFINITION) 1.6 fix x y 1.7 - assume "Rep x = Rep y" 1.8 + assume b: "Rep x = Rep y" 1.9 from td have "x = Abs (Rep x)" 1.10 by auto 1.11 also have "Abs (Rep x) = Abs (Rep y)" 1.12 - by (simp add: prems) 1.13 + by (simp add: b) 1.14 also from td have "Abs (Rep y) = y" 1.15 by auto 1.16 finally show "x = y" .