equal
deleted
inserted
replaced
136 (** tracing *) |
136 (** tracing *) |
137 |
137 |
138 val trace_rules = ref false; |
138 val trace_rules = ref false; |
139 |
139 |
140 fun trace ctxt rules = |
140 fun trace ctxt rules = |
141 if not (! trace_rules) orelse null rules then () |
141 conditional (! trace_rules andalso not (null rules)) (fn () => |
142 else Pretty.writeln (Pretty.big_list "rules:" (map (ProofContext.pretty_thm ctxt) rules)); |
142 Pretty.big_list "rules:" (map (ProofContext.pretty_thm ctxt) rules) |
|
143 |> Pretty.string_of |> tracing); |
143 |
144 |
144 |
145 |
145 |
146 |
146 (** global and local rule data **) |
147 (** global and local rule data **) |
147 |
148 |