reactivated theory Class;
authorwenzelm
Wed Jun 13 14:21:54 2007 +0200 (2007-06-13)
changeset 23371ed60e560048d
parent 23370 513a8ee192f1
child 23372 0035be079bee
reactivated theory Class;
src/HOL/Nominal/Examples/ROOT.ML
     1.1 --- a/src/HOL/Nominal/Examples/ROOT.ML	Wed Jun 13 12:22:02 2007 +0200
     1.2 +++ b/src/HOL/Nominal/Examples/ROOT.ML	Wed Jun 13 14:21:54 2007 +0200
     1.3 @@ -5,9 +5,9 @@
     1.4  Various examples involving nominal datatypes.
     1.5  *)
     1.6  
     1.7 -(*use_thy "Class";*)
     1.8  use_thy "CR";
     1.9  use_thy "CR_Takahashi";
    1.10 +use_thy "Class";
    1.11  use_thy "Compile";
    1.12  use_thy "Fsub";
    1.13  use_thy "Height";