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