Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
generic_merge;
authorwenzelm
Sat, 24 Nov 2001 16:54:32 +0100
changeset 12282 f98beaaa7c4f
parent 12281 3bd113b8f7a6
child 12283 d42aa776889e
generic_merge;
src/Provers/simplifier.ML file | annotate | diff | comparison | revisions 
--- a/src/Provers/simplifier.ML	Sat Nov 24 16:54:10 2001 +0100
+++ b/src/Provers/simplifier.ML	Sat Nov 24 16:54:32 2001 +0100
@@ -134,11 +134,10 @@
 
 datatype solver = Solver of string * (thm list -> int -> tactic) * stamp;
 
-fun mk_solver name solver = Solver(name, solver, stamp());
+fun mk_solver name solver = Solver (name, solver, stamp());
+fun eq_solver (Solver (_, _, s1), Solver(_, _, s2)) = s1 = s2;
 
-fun eq_solver (Solver(_,_,s1),Solver(_,_,s2)) = s1=s2;
-
-val merge_solvers = generic_merge eq_solver I I;
+val merge_solvers = gen_merge_lists eq_solver;
 
 fun app_sols [] _ _ = no_tac
   | app_sols (Solver(_,solver,_)::sols) thms i =
isabelle