equal
deleted
inserted
replaced
292 end; |
292 end; |
293 |
293 |
294 val _ = |
294 val _ = |
295 print_function "print_state" |
295 print_function "print_state" |
296 (fn {command_name, ...} => |
296 (fn {command_name, ...} => |
297 SOME {delay = NONE, pri = 1, persistent = true, strict = true, |
297 SOME {delay = NONE, pri = 1, persistent = false, strict = true, |
298 print_fn = fn tr => fn st' => |
298 print_fn = fn tr => fn st' => |
299 let |
299 let |
300 val is_init = Keyword.is_theory_begin command_name; |
300 val is_init = Keyword.is_theory_begin command_name; |
301 val is_proof = Keyword.is_proof command_name; |
301 val is_proof = Keyword.is_proof command_name; |
302 val do_print = |
302 val do_print = |