equal
deleted
inserted
replaced
16 structure Boogie_Split: BOOGIE_SPLIT = |
16 structure Boogie_Split: BOOGIE_SPLIT = |
17 struct |
17 struct |
18 |
18 |
19 (* sub-tactics store *) |
19 (* sub-tactics store *) |
20 |
20 |
21 structure Sub_Tactics = TheoryDataFun |
21 structure Sub_Tactics = Theory_Data |
22 ( |
22 ( |
23 type T = (Proof.context -> int -> tactic) Symtab.table |
23 type T = (Proof.context -> int -> tactic) Symtab.table |
24 val empty = Symtab.empty |
24 val empty = Symtab.empty |
25 val copy = I |
|
26 val extend = I |
25 val extend = I |
27 fun merge _ = Symtab.merge (K true) |
26 fun merge data = Symtab.merge (K true) data |
28 ) |
27 ) |
29 |
28 |
30 fun add_sub_tactic tac = Sub_Tactics.map (Symtab.update_new tac) |
29 fun add_sub_tactic tac = Sub_Tactics.map (Symtab.update_new tac) |
31 |
30 |
32 val sub_tactic_names = Symtab.keys o Sub_Tactics.get |
31 val sub_tactic_names = Symtab.keys o Sub_Tactics.get |