--- a/Nominal/Nominal2.thy	Wed Jan 05 16:51:27 2011 +0000
+++ b/Nominal/Nominal2.thy	Wed Jan 05 17:33:43 2011 +0000
@@ -5,6 +5,7 @@
      ("nominal_dt_alpha.ML")
      ("nominal_dt_quot.ML")
      ("nominal_induct.ML")
+     ("nominal_inductive.ML") 
 begin
 
 
@@ -17,6 +18,8 @@
 use "nominal_dt_quot.ML"
 ML {* open Nominal_Dt_Quot *}
 
+
+
 (*****************************************)
 (* setup for induction principles method *)
 use "nominal_induct.ML"
@@ -24,6 +27,11 @@
   {* NominalInduct.nominal_induct_method *}
   {* nominal induction *}
 
+(****************************************************)
+(* inductive definition involving nominal datatypes *)
+use "nominal_inductive.ML" 
+
+
 ML {*
 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
 val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add)