src/HOL/Old_Number_Theory/WilsonRuss.thy
changeset 42793 88bee9f6eec7
parent 39159 0dec18004e75
child 44766 d4d33a4d7548
     1.1 --- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Fri May 13 16:03:03 2011 +0200
     1.2 +++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Fri May 13 22:55:00 2011 +0200
     1.3 @@ -264,7 +264,7 @@
     1.4         apply (simp add: zmult_assoc)
     1.5        apply (rule_tac [5] zcong_zmult)
     1.6         apply (rule_tac [5] inv_is_inv)
     1.7 -         apply (tactic "clarify_tac @{claset} 4")
     1.8 +         apply (tactic "clarify_tac @{context} 4")
     1.9           apply (subgoal_tac [4] "a \<in> wset (a - 1) p")
    1.10            apply (rule_tac [5] wset_inv_mem_mem)
    1.11                 apply (simp_all add: wset_fin)