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.
type_solver_tac: use TCSET' to refer to context of goal state (does
authorwenzelm
Thu, 15 Nov 2001 18:21:38 +0100
changeset 12209 09bc6f8456b9
parent 12208 5efe7b6874fd
child 12210 2f510d8d8291
type_solver_tac: use TCSET' to refer to context of goal state (does *not* work with local proof contexts of Isar / new-style locales);
src/ZF/simpdata.ML file | annotate | diff | comparison | revisions 
--- a/src/ZF/simpdata.ML	Thu Nov 15 18:20:48 2001 +0100
+++ b/src/ZF/simpdata.ML	Thu Nov 15 18:21:38 2001 +0100
@@ -45,10 +45,12 @@
 
 val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
 
-simpset_ref() := simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
-                           addcongs [if_weak_cong]
-		           addsplits [split_if]
-                           setSolver (mk_solver "types" Type_solver_tac);
+simpset_ref() :=
+  simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
+  addcongs [if_weak_cong]
+  addsplits [split_if]
+  setSolver (mk_solver "types" (fn prems => TCSET' (fn tcset => type_solver_tac tcset prems)));
+
 
 (** Splitting IFs in the assumptions **)
isabelle