equal
deleted
inserted
replaced
2 Author: Sebastian Skalberg (TU Muenchen) |
2 Author: Sebastian Skalberg (TU Muenchen) |
3 *) |
3 *) |
4 |
4 |
5 signature IMPORT = |
5 signature IMPORT = |
6 sig |
6 sig |
7 val debug : bool ref |
7 val debug : bool Unsynchronized.ref |
8 val import_tac : Proof.context -> string * string -> tactic |
8 val import_tac : Proof.context -> string * string -> tactic |
9 val setup : theory -> theory |
9 val setup : theory -> theory |
10 end |
10 end |
11 |
11 |
12 structure ImportData = TheoryDataFun |
12 structure ImportData = TheoryDataFun |
19 ) |
19 ) |
20 |
20 |
21 structure Import :> IMPORT = |
21 structure Import :> IMPORT = |
22 struct |
22 struct |
23 |
23 |
24 val debug = ref false |
24 val debug = Unsynchronized.ref false |
25 fun message s = if !debug then writeln s else () |
25 fun message s = if !debug then writeln s else () |
26 |
26 |
27 fun import_tac ctxt (thyname, thmname) = |
27 fun import_tac ctxt (thyname, thmname) = |
28 if ! quick_and_dirty |
28 if ! quick_and_dirty |
29 then SkipProof.cheat_tac (ProofContext.theory_of ctxt) |
29 then SkipProof.cheat_tac (ProofContext.theory_of ctxt) |