# HG changeset patch
# User paulson
# Date 1136809714 -3600
# Node ID 2e7afae14fa5fffe84573314eda8f493e40e90ef
# Parent  9a5419d5ca01b74a787e8326921f105c40ba3f4a
tidied

diff -r 9a5419d5ca01 -r 2e7afae14fa5 src/HOL/Integ/NatSimprocs.thy
--- a/src/HOL/Integ/NatSimprocs.thy	Mon Jan 09 13:28:06 2006 +0100
+++ b/src/HOL/Integ/NatSimprocs.thy	Mon Jan 09 13:28:34 2006 +0100
@@ -35,8 +35,8 @@
      "neg (number_of (bin_minus v)::int) ==>  
       Suc m - (number_of v) = m - (number_of (bin_pred v))"
 apply (subst Suc_diff_eq_diff_pred)
-apply (simp add: ); 
-apply (simp del: nat_numeral_1_eq_1); 
+apply simp
+apply (simp del: nat_numeral_1_eq_1)
 apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric] 
                         neg_number_of_bin_pred_iff_0)
 done
@@ -360,7 +360,8 @@
      "(0 < r/2) = (0 < (r::'a::{ordered_field,division_by_zero,number_ring}))"
 by auto
 
-lemmas half_gt_zero = half_gt_zero_iff [THEN iffD2, simp]
+lemmas half_gt_zero = half_gt_zero_iff [THEN iffD2]
+declare half_gt_zero [simp]
 
 (* The following lemma should appear in Divides.thy, but there the proof
    doesn't work. *)