equal
deleted
inserted
replaced
119 Args.$$$ "no_quantify" >> (K (K false)); |
119 Args.$$$ "no_quantify" >> (K (K false)); |
120 in |
120 in |
121 Method.simple_args |
121 Method.simple_args |
122 (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >> |
122 (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >> |
123 curry (Library.foldl op |>) true) |
123 curry (Library.foldl op |>) true) |
124 (fn q => fn ctxt => meth ctxt q 1) |
124 (fn q => fn ctxt => meth ctxt q) |
125 end; |
125 end; |
126 |
126 |
127 fun linz_method ctxt q i = Method.METHOD (fn facts => |
127 fun linz_method ctxt q = SIMPLE_METHOD' (linz_tac ctxt q); |
128 Method.insert_tac facts 1 THEN linz_tac ctxt q i); |
|
129 |
128 |
130 val setup = |
129 val setup = |
131 Method.add_method ("cooper", |
130 Method.add_method ("cooper", |
132 linz_args linz_method, |
131 linz_args linz_method, |
133 "decision procedure for linear integer arithmetic"); |
132 "decision procedure for linear integer arithmetic"); |