src/ZF/ind_syntax.ML

 (*The structure protects these items from redeclaration (somewhat!).  The 
   datatype definitions in theory files refer to these items by name!
 *)
 structure Ind_Syntax =
 struct
+
+(*Print tracing messages during processing of "inductive" theory sections*)
+val trace = ref false;
 
 (** Abstract syntax definitions for ZF **)
 
 val iT = Type("i",[]);
 

 (*Turns iff rules into safe elimination rules*)
 fun mk_free_SEs iffs = map (gen_make_elim [conjE,FalseE]) (iffs RL [iffD1]);
 
 end;
 
+
+val trace_induct = Ind_Syntax.trace;