equal
deleted
inserted
replaced
39 val description = "arith facts - only ground formulas" |
39 val description = "arith facts - only ground formulas" |
40 ); |
40 ); |
41 |
41 |
42 val get_arith_facts = Arith_Facts.get; |
42 val get_arith_facts = Arith_Facts.get; |
43 |
43 |
44 structure Arith_Tactics = TheoryDataFun |
44 structure Arith_Tactics = Theory_Data |
45 ( |
45 ( |
46 type T = (serial * (string * (bool -> Proof.context -> int -> tactic))) list; |
46 type T = (serial * (string * (bool -> Proof.context -> int -> tactic))) list; |
47 val empty = []; |
47 val empty = []; |
48 val copy = I; |
|
49 val extend = I; |
48 val extend = I; |
50 fun merge _ = AList.merge (op =) (K true); |
49 fun merge data : T = AList.merge (op =) (K true) data; |
51 ); |
50 ); |
52 |
51 |
53 fun add_tactic name tac = Arith_Tactics.map (cons (serial (), (name, tac))); |
52 fun add_tactic name tac = Arith_Tactics.map (cons (serial (), (name, tac))); |
54 |
53 |
55 fun gen_arith_tac verbose ctxt = |
54 fun gen_arith_tac verbose ctxt = |