equal
deleted
inserted
replaced
23 struct |
23 struct |
24 |
24 |
25 val debug = ref false |
25 val debug = ref false |
26 fun message s = if !debug then writeln s else () |
26 fun message s = if !debug then writeln s else () |
27 |
27 |
28 val string_of_thm = PrintMode.setmp [] string_of_thm; |
28 val string_of_thm = PrintMode.setmp [] Display.string_of_thm; |
29 val string_of_cterm = PrintMode.setmp [] string_of_cterm; |
29 val string_of_cterm = PrintMode.setmp [] Display.string_of_cterm; |
30 |
30 |
31 fun import_tac (thyname,thmname) = |
31 fun import_tac (thyname,thmname) = |
32 if ! quick_and_dirty |
32 if ! quick_and_dirty |
33 then SkipProof.cheat_tac |
33 then SkipProof.cheat_tac |
34 else |
34 else |