author | Christian Urban <urbanc@in.tum.de> |
Thu, 12 Aug 2010 21:29:35 +0800 | |
changeset 2396 | f2f611daf480 |
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