Nominal/Perm.thy
changeset 2305 93ab397f5980
parent 2302 c6db12ddb60c
child 2335 558c823f96aa
equal deleted inserted replaced
2304:8a98171ba1fc 2305:93ab397f5980
     3   "../Nominal-General/Nominal2_Base"
     3   "../Nominal-General/Nominal2_Base"
     4   "../Nominal-General/Nominal2_Atoms" 
     4   "../Nominal-General/Nominal2_Atoms" 
     5   "../Nominal-General/Nominal2_Eqvt" 
     5   "../Nominal-General/Nominal2_Eqvt" 
     6   "Nominal2_FSet"
     6   "Nominal2_FSet"
     7   "Abs"
     7   "Abs"
     8 (*uses ("nominal_dt_rawperm.ML")
     8 uses ("nominal_dt_rawperm.ML")
     9      ("nominal_dt_rawfuns.ML")
     9      ("nominal_dt_rawfuns.ML")
    10      ("nominal_dt_alpha.ML")*)
    10      ("nominal_dt_alpha.ML")
    11 begin
    11 begin
    12 
    12 
    13 use "nominal_dt_rawperm.ML"
    13 use "nominal_dt_rawperm.ML"
    14 ML {* open Nominal_Dt_RawPerm *}
    14 ML {* open Nominal_Dt_RawPerm *}
    15 
    15