src/HOL/Word/Word.thy
changeset 54742 7a86358a3c0b
parent 54489 03ff4d1e6784
child 54743 b9ae4a2f615b
     1.1 --- a/src/HOL/Word/Word.thy	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/HOL/Word/Word.thy	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -1463,7 +1463,7 @@
     1.4          (put_simpset HOL_ss ctxt
     1.5            |> fold Splitter.add_split @{thms uint_splits}
     1.6            |> fold Simplifier.add_cong @{thms power_False_cong})),
     1.7 -      rewrite_goals_tac @{thms word_size}, 
     1.8 +      rewrite_goals_tac ctxt @{thms word_size}, 
     1.9        ALLGOALS  (fn n => REPEAT (resolve_tac [allI, impI] n) THEN      
    1.10                           REPEAT (etac conjE n) THEN
    1.11                           REPEAT (dtac @{thm word_of_int_inverse} n 
    1.12 @@ -1964,7 +1964,7 @@
    1.13          (put_simpset HOL_ss ctxt
    1.14            |> fold Splitter.add_split @{thms unat_splits}
    1.15            |> fold Simplifier.add_cong @{thms power_False_cong})),
    1.16 -      rewrite_goals_tac @{thms word_size}, 
    1.17 +      rewrite_goals_tac ctxt @{thms word_size}, 
    1.18        ALLGOALS  (fn n => REPEAT (resolve_tac [allI, impI] n) THEN      
    1.19                           REPEAT (etac conjE n) THEN
    1.20                           REPEAT (dtac @{thm of_nat_inverse} n THEN atac n)),