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" .