equal
deleted
inserted
replaced
63 val verbose_arith_tac = gen_arith_tac true; |
63 val verbose_arith_tac = gen_arith_tac true; |
64 |
64 |
65 val setup = |
65 val setup = |
66 Arith_Facts.setup #> |
66 Arith_Facts.setup #> |
67 Method.setup @{binding arith} |
67 Method.setup @{binding arith} |
68 (Args.bang_facts >> (fn prems => fn ctxt => |
68 (Scan.succeed (fn ctxt => |
69 METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ get_arith_facts ctxt @ facts) |
69 METHOD (fn facts => HEADGOAL (Method.insert_tac (get_arith_facts ctxt @ facts) |
70 THEN' verbose_arith_tac ctxt)))) |
70 THEN' verbose_arith_tac ctxt)))) |
71 "various arithmetic decision procedures"; |
71 "various arithmetic decision procedures"; |
72 |
72 |
73 |
73 |
74 (* some specialized syntactic operations *) |
74 (* some specialized syntactic operations *) |