src/Provers/simplifier.ML
changeset 12282 f98beaaa7c4f
parent 12109 bd6eb9194a5d
child 12311 ce5f9e61c037
equal deleted inserted replaced
12281:3bd113b8f7a6 12282:f98beaaa7c4f
   132 
   132 
   133 (** solvers **)
   133 (** solvers **)
   134 
   134 
   135 datatype solver = Solver of string * (thm list -> int -> tactic) * stamp;
   135 datatype solver = Solver of string * (thm list -> int -> tactic) * stamp;
   136 
   136 
   137 fun mk_solver name solver = Solver(name, solver, stamp());
   137 fun mk_solver name solver = Solver (name, solver, stamp());
   138 
   138 fun eq_solver (Solver (_, _, s1), Solver(_, _, s2)) = s1 = s2;
   139 fun eq_solver (Solver(_,_,s1),Solver(_,_,s2)) = s1=s2;
   139 
   140 
   140 val merge_solvers = gen_merge_lists eq_solver;
   141 val merge_solvers = generic_merge eq_solver I I;
       
   142 
   141 
   143 fun app_sols [] _ _ = no_tac
   142 fun app_sols [] _ _ = no_tac
   144   | app_sols (Solver(_,solver,_)::sols) thms i =
   143   | app_sols (Solver(_,solver,_)::sols) thms i =
   145        solver thms i ORELSE app_sols sols thms i;
   144        solver thms i ORELSE app_sols sols thms i;
   146 
   145