Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Sequents/simpdata.ML
changeset 7570 a9391550eea1
parent 7123 4ab38de3fd20
child 9259 103acc345f75 
--- a/src/Sequents/simpdata.ML	Tue Sep 21 19:10:39 1999 +0200
+++ b/src/Sequents/simpdata.ML	Tue Sep 21 19:11:07 1999 +0200
@@ -241,8 +241,8 @@
 
 (*No simprules, but basic infrastructure for simplification*)
 val LK_basic_ss = empty_ss setsubgoaler asm_simp_tac
-			   setSSolver   safe_solver
-			   setSolver    unsafe_solver
+			   setSSolver   (mk_solver "safe" safe_solver)
+			   setSolver    (mk_solver "unsafe" unsafe_solver)
 			   setmksimps   (map mk_meta_eq o atomize o gen_all);
 
 val LK_simps =
isabelle