src/HOL/Library/Countable.thy
changeset 26580 c3e597a476fd
parent 26350 a170a190c5d3
child 26585 3bf2ebb7148e
--- a/src/HOL/Library/Countable.thy	Tue Apr 08 15:47:15 2008 +0200
+++ b/src/HOL/Library/Countable.thy	Tue Apr 08 18:30:40 2008 +0200
@@ -121,7 +121,7 @@
   obtains (zero) "(z::int) = 0" "sgn z = 0" "abs z = 0"
   | (pos) n where "z = of_nat n" "sgn z = 1" "abs z = of_nat n"
   | (neg) n where "z = - (of_nat n)" "sgn z = -1" "abs z = of_nat n"
-apply elim_to_cases
+apply atomize_elim
 apply (insert int_cases[of z])
 apply (auto simp:zsgn_def)
 apply (rule_tac x="nat (-z)" in exI, simp)