# HG changeset patch
# User wenzelm
# Date 974573137 -3600
# Node ID 0054c785f49541b3615f7de27ecb0109abea7fce
# Parent  a4684cf28edf796a00a82a7c250cccdc92318ff9
abs_eq_0: #0 instead of 0;

diff -r a4684cf28edf -r 0054c785f495 src/HOL/Integ/IntArith.ML
--- a/src/HOL/Integ/IntArith.ML	Sat Nov 18 19:45:05 2000 +0100
+++ b/src/HOL/Integ/IntArith.ML	Sat Nov 18 19:45:37 2000 +0100
@@ -108,7 +108,7 @@
 by (simp_tac (simpset () addsplits [zabs_split] addsimps [zmult_less_0_iff, zle_def]) 1);
 qed "abs_mult";
 
-Goal "(abs x = 0) = (x = (0::int))";
+Goal "(abs x = #0) = (x = (#0::int))";
 by (simp_tac (simpset () addsplits [zabs_split]) 1);
 qed "abs_eq_0";
 AddIffs [abs_eq_0];