equal
deleted
inserted
replaced
46 Theory.setup |
46 Theory.setup |
47 (Method.setup @{binding arith} |
47 (Method.setup @{binding arith} |
48 (Scan.succeed (fn ctxt => |
48 (Scan.succeed (fn ctxt => |
49 METHOD (fn facts => |
49 METHOD (fn facts => |
50 HEADGOAL |
50 HEADGOAL |
51 (Method.insert_tac (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts) |
51 (Method.insert_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts) |
52 THEN' arith_tac ctxt)))) |
52 THEN' arith_tac ctxt)))) |
53 "various arithmetic decision procedures"); |
53 "various arithmetic decision procedures"); |
54 |
54 |
55 |
55 |
56 (* some specialized syntactic operations *) |
56 (* some specialized syntactic operations *) |
57 |
57 |