changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
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