src/HOL/Decision_Procs/cooper_tac.ML
changeset 30509 e19d5b459a61
parent 30439 57c68b3af2ea
child 30939 207ec81543f6
equal deleted inserted replaced
30508:958cc116d03b 30509:e19d5b459a61
   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");