# HG changeset patch
# User paulson
# Date 957458391 -7200
# Node ID 3b10d24b5eddfa13404ddae42310788577c98f88
# Parent  6b524f8c2a2ccb1783925f2eeb1ee335f7c0a342
a safer way of proving literal equalities

diff -r 6b524f8c2a2c -r 3b10d24b5edd src/HOL/Integ/NatBin.ML
--- a/src/HOL/Integ/NatBin.ML	Thu May 04 15:17:41 2000 +0200
+++ b/src/HOL/Integ/NatBin.ML	Thu May 04 18:39:51 2000 +0200
@@ -225,13 +225,15 @@
 
 (*"neg" is used in rewrite rules for binary comparisons*)
 Goal "((number_of v :: nat) = number_of v') = \
-\        (if neg (number_of v) then ((#0::nat) = number_of v') \
-\         else if neg (number_of v') then iszero (number_of v) \
-\         else iszero (number_of (bin_add v (bin_minus v'))))";
+\     (if neg (number_of v) then (iszero (number_of v') | neg (number_of v')) \
+\      else if neg (number_of v') then iszero (number_of v) \
+\      else iszero (number_of (bin_add v (bin_minus v'))))";
 by (simp_tac
     (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
 				  eq_nat_nat_iff, eq_number_of_eq, nat_0]) 1);
-by (simp_tac (simpset_of Int.thy addsimps [nat_eq_iff, iszero_def]) 1);
+by (simp_tac (simpset_of Int.thy addsimps [nat_eq_iff, nat_eq_iff2, 
+					   iszero_def]) 1);
+by (simp_tac (simpset_of Int.thy addsimps [not_neg_eq_ge_0 RS sym]) 1);
 qed "eq_nat_number_of";
 
 Addsimps [eq_nat_number_of];