src/ZF/ind_syntax.ML
changeset 4804 02b7c759159b
parent 4352 7ac9f3e8a97d
child 4972 7fe1d30c1374
     1.1 --- a/src/ZF/ind_syntax.ML	Thu Apr 09 12:31:35 1998 +0200
     1.2 +++ b/src/ZF/ind_syntax.ML	Fri Apr 10 13:15:28 1998 +0200
     1.3 @@ -12,6 +12,9 @@
     1.4  structure Ind_Syntax =
     1.5  struct
     1.6  
     1.7 +(*Print tracing messages during processing of "inductive" theory sections*)
     1.8 +val trace = ref false;
     1.9 +
    1.10  (** Abstract syntax definitions for ZF **)
    1.11  
    1.12  val iT = Type("i",[]);
    1.13 @@ -124,3 +127,5 @@
    1.14  
    1.15  end;
    1.16  
    1.17 +
    1.18 +val trace_induct = Ind_Syntax.trace;