tuned
authorhaftmann
Thu Oct 13 22:56:19 2011 +0200 (2011-10-13 ago)
changeset 45138ba618e9288b8
parent 45137 6e422d180de8
child 45139 bdcaa3f3a2f4
tuned
src/HOL/UNITY/UNITY_tactics.ML
     1.1 --- a/src/HOL/UNITY/UNITY_tactics.ML	Thu Oct 13 22:56:19 2011 +0200
     1.2 +++ b/src/HOL/UNITY/UNITY_tactics.ML	Thu Oct 13 22:56:19 2011 +0200
     1.3 @@ -46,7 +46,7 @@
     1.4        ORELSE res_inst_tac ctxt
     1.5          [(("act", 0), sact)] @{thm transientI} 2,
     1.6           (*simplify the command's domain*)
     1.7 -      simp_tac (simpset_of ctxt addsimps [@{thm Domain_def}]) 3,
     1.8 +      simp_tac (simpset_of ctxt addsimps @{thms Domain_def}) 3,
     1.9        constrains_tac ctxt 1,
    1.10        ALLGOALS (clarify_tac ctxt),
    1.11        ALLGOALS (asm_lr_simp_tac (simpset_of ctxt))]);