src/HOL/Nominal/Examples/ROOT.ML
changeset 23371 ed60e560048d
parent 23283 c7ab7051aba0
child 24153 1a4607b7ad24
equal deleted inserted replaced
23370:513a8ee192f1 23371:ed60e560048d
     3     Author:     Christian Urban, TU Muenchen
     3     Author:     Christian Urban, TU Muenchen
     4 
     4 
     5 Various examples involving nominal datatypes.
     5 Various examples involving nominal datatypes.
     6 *)
     6 *)
     7 
     7 
     8 (*use_thy "Class";*)
       
     9 use_thy "CR";
     8 use_thy "CR";
    10 use_thy "CR_Takahashi";
     9 use_thy "CR_Takahashi";
       
    10 use_thy "Class";
    11 use_thy "Compile";
    11 use_thy "Compile";
    12 use_thy "Fsub";
    12 use_thy "Fsub";
    13 use_thy "Height";
    13 use_thy "Height";
    14 use_thy "Lambda_mu";
    14 use_thy "Lambda_mu";
    15 use_thy "SN";
    15 use_thy "SN";