changeset 4804 | 02b7c759159b |
parent 4352 | 7ac9f3e8a97d |
child 4972 | 7fe1d30c1374 |
--- a/src/ZF/ind_syntax.ML Thu Apr 09 12:31:35 1998 +0200 +++ b/src/ZF/ind_syntax.ML Fri Apr 10 13:15:28 1998 +0200 @@ -12,6 +12,9 @@ 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",[]); @@ -124,3 +127,5 @@ end; + +val trace_induct = Ind_Syntax.trace;