equal
deleted
inserted
replaced
836 |
836 |
837 |
837 |
838 fun maxthy thy1 thy2 = if Context.subthy (thy1, thy2) then thy2 else thy1; |
838 fun maxthy thy1 thy2 = if Context.subthy (thy1, thy2) then thy2 else thy1; |
839 |
839 |
840 |
840 |
|
841 (* trace internal steps of isac's numeral calculations *) |
|
842 val trace_calc = Unsynchronized.ref false; |
841 (*.trace internal steps of isac's rewriter*) |
843 (*.trace internal steps of isac's rewriter*) |
842 val trace_rewrite = Unsynchronized.ref false; |
844 val trace_rewrite = Unsynchronized.ref false; |
843 (*.depth of recursion in traces of the rewriter, if trace_rewrite:=true.*) |
845 (*.depth of recursion in traces of the rewriter, if trace_rewrite:=true.*) |
844 val depth = Unsynchronized.ref 99999; |
846 val depth = Unsynchronized.ref 99999; |
845 (*.no of rewrites exceeding this int -> NO rewrite.*) |
847 (*.no of rewrites exceeding this int -> NO rewrite.*) |