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/HOL/UNITY/UNITY_tactics.ML
changeset 45138 ba618e9288b8
parent 42795 66fcc9882784
child 46752 e9e7209eb375 
--- a/src/HOL/UNITY/UNITY_tactics.ML	Thu Oct 13 22:56:19 2011 +0200
+++ b/src/HOL/UNITY/UNITY_tactics.ML	Thu Oct 13 22:56:19 2011 +0200
@@ -46,7 +46,7 @@
       ORELSE res_inst_tac ctxt
         [(("act", 0), sact)] @{thm transientI} 2,
          (*simplify the command's domain*)
-      simp_tac (simpset_of ctxt addsimps [@{thm Domain_def}]) 3,
+      simp_tac (simpset_of ctxt addsimps @{thms Domain_def}) 3,
       constrains_tac ctxt 1,
       ALLGOALS (clarify_tac ctxt),
       ALLGOALS (asm_lr_simp_tac (simpset_of ctxt))]);
isabelle