src/HOL/Word/WordArith.thy
changeset 30607 c3d1590debd8
parent 30549 d2d7874648bd
child 30649 57753e0ec1d4
     1.1 --- a/src/HOL/Word/WordArith.thy	Fri Mar 20 11:26:59 2009 +0100
     1.2 +++ b/src/HOL/Word/WordArith.thy	Fri Mar 20 15:24:18 2009 +0100
     1.3 @@ -511,10 +511,13 @@
     1.4       addcongs @{thms power_False_cong}
     1.5  
     1.6  fun uint_arith_tacs ctxt = 
     1.7 -  let fun arith_tac' n t = arith_tac ctxt n t handle COOPER => Seq.empty  
     1.8 +  let
     1.9 +    fun arith_tac' n t = arith_tac ctxt n t handle COOPER => Seq.empty;
    1.10 +    val cs = local_claset_of ctxt;
    1.11 +    val ss = local_simpset_of ctxt;
    1.12    in 
    1.13 -    [ CLASET' clarify_tac 1,
    1.14 -      SIMPSET' (full_simp_tac o uint_arith_ss_of) 1,
    1.15 +    [ clarify_tac cs 1,
    1.16 +      full_simp_tac (uint_arith_ss_of ss) 1,
    1.17        ALLGOALS (full_simp_tac (HOL_ss addsplits @{thms uint_splits} 
    1.18                                        addcongs @{thms power_False_cong})),
    1.19        rewrite_goals_tac @{thms word_size}, 
    1.20 @@ -1069,10 +1072,13 @@
    1.21       addcongs @{thms power_False_cong}
    1.22  
    1.23  fun unat_arith_tacs ctxt =   
    1.24 -  let fun arith_tac' n t = arith_tac ctxt n t handle COOPER => Seq.empty  
    1.25 +  let
    1.26 +    fun arith_tac' n t = arith_tac ctxt n t handle COOPER => Seq.empty;
    1.27 +    val cs = local_claset_of ctxt;
    1.28 +    val ss = local_simpset_of ctxt;
    1.29    in 
    1.30 -    [ CLASET' clarify_tac 1,
    1.31 -      SIMPSET' (full_simp_tac o unat_arith_ss_of) 1,
    1.32 +    [ clarify_tac cs 1,
    1.33 +      full_simp_tac (unat_arith_ss_of ss) 1,
    1.34        ALLGOALS (full_simp_tac (HOL_ss addsplits @{thms unat_splits} 
    1.35                                         addcongs @{thms power_False_cong})),
    1.36        rewrite_goals_tac @{thms word_size},