author | Christian Urban <urbanc@in.tum.de> |
Sat, 10 Jul 2010 11:27:04 +0100 | |
changeset 2351 | 842969a598f2 |
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