author | Christian Urban <urbanc@in.tum.de> |
Sun, 18 Jul 2010 19:07:05 +0100 | |
changeset 2371 | 86c73a06ba4b |
parent 2346 | 4c5881455923 |
permissions | -rw-r--r-- |
theory Perm imports "../Nominal-General/Nominal2_Base" "../Nominal-General/Nominal2_Atoms" "../Nominal-General/Nominal2_Eqvt" "Nominal2_FSet" "Abs" uses ("nominal_dt_rawperm.ML") ("nominal_dt_rawfuns.ML") ("nominal_dt_alpha.ML") ("nominal_dt_quot.ML") begin use "nominal_dt_rawperm.ML" ML {* open Nominal_Dt_RawPerm *} use "nominal_dt_rawfuns.ML" ML {* open Nominal_Dt_RawFuns *} use "nominal_dt_alpha.ML" ML {* open Nominal_Dt_Alpha *} use "nominal_dt_quot.ML" ML {* open Nominal_Dt_Quot *} end