author | Christian Urban <urbanc@in.tum.de> |
Sun, 22 Aug 2010 12:36:53 +0800 | |
changeset 2429 | b29eb13d3f9d |
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