changeset 2595 | 07f775729e90 |
parent 2594 | 515e5496171c |
child 2598 | b136721eedb2 |
--- a/Nominal/Nominal2.thy Mon Dec 06 16:35:42 2010 +0000 +++ b/Nominal/Nominal2.thy Mon Dec 06 17:11:34 2010 +0000 @@ -5,7 +5,6 @@ ("nominal_dt_rawfuns.ML") ("nominal_dt_alpha.ML") ("nominal_dt_quot.ML") - ("nominal_dt_supp.ML") begin use "nominal_dt_rawperm.ML" @@ -20,8 +19,6 @@ use "nominal_dt_quot.ML" ML {* open Nominal_Dt_Quot *} -use "nominal_dt_supp.ML" -ML {* open Nominal_Dt_Supp *} section{* Interface for nominal_datatype *}