discontinued obsolete alias HOL.thy for @{theory HOL} in ML;
authorwenzelm
Tue Feb 08 20:59:12 2011 +0100 (2011-02-08)
changeset 41732996b0c14a430
parent 41731 2fb760843e17
child 41733 775da08dae1b
discontinued obsolete alias HOL.thy for @{theory HOL} in ML;
src/HOL/Typedef.thy
     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"