src/HOL/Typedef.thy
changeset 41732 996b0c14a430
parent 38536 7e57a0dcbd4f
child 46947 b8c7eb0c2f89
     1.1 --- a/src/HOL/Typedef.thy	Tue Feb 08 19:57:11 2011 +0100
     1.2 +++ b/src/HOL/Typedef.thy	Tue Feb 08 20:59:12 2011 +0100
     1.3 @@ -9,10 +9,6 @@
     1.4  uses ("Tools/typedef.ML")
     1.5  begin
     1.6  
     1.7 -ML {*
     1.8 -structure HOL = struct val thy = @{theory HOL} end;
     1.9 -*}  -- "belongs to theory HOL"
    1.10 -
    1.11  locale type_definition =
    1.12    fixes Rep and Abs and A
    1.13    assumes Rep: "Rep x \<in> A"