# HG changeset patch
# User paulson
# Date 1136973595 -3600
# Node ID 22f96cd085d51e9641d0899c4bbb420cda9e7fd8
# Parent  5f5d37e763c49131b05e7d90326eedc59889b7e2
tidied, and giving theorems names

diff -r 5f5d37e763c4 -r 22f96cd085d5 src/HOL/Integ/IntDiv.thy
--- a/src/HOL/Integ/IntDiv.thy	Wed Jan 11 03:10:04 2006 +0100
+++ b/src/HOL/Integ/IntDiv.thy	Wed Jan 11 10:59:55 2006 +0100
@@ -250,16 +250,19 @@
 apply (auto simp add: quorem_def mod_def)
 done
 
-lemmas pos_mod_sign[simp]  = pos_mod_conj [THEN conjunct1, standard]
-   and pos_mod_bound[simp] = pos_mod_conj [THEN conjunct2, standard]
+lemmas pos_mod_sign  = pos_mod_conj [THEN conjunct1, standard]
+   and pos_mod_bound = pos_mod_conj [THEN conjunct2, standard]
+
+declare pos_mod_sign[simp] pos_mod_bound[simp]
 
 lemma neg_mod_conj : "b < (0::int) ==> a mod b \<le> 0 & b < a mod b"
 apply (cut_tac a = a and b = b in divAlg_correct)
 apply (auto simp add: quorem_def div_def mod_def)
 done
 
-lemmas neg_mod_sign[simp]  = neg_mod_conj [THEN conjunct1, standard]
-   and neg_mod_bound[simp] = neg_mod_conj [THEN conjunct2, standard]
+lemmas neg_mod_sign  = neg_mod_conj [THEN conjunct1, standard]
+   and neg_mod_bound = neg_mod_conj [THEN conjunct2, standard]
+declare neg_mod_sign[simp] neg_mod_bound[simp]
 
 
 
diff -r 5f5d37e763c4 -r 22f96cd085d5 src/HOL/Integ/NatSimprocs.thy
--- a/src/HOL/Integ/NatSimprocs.thy	Wed Jan 11 03:10:04 2006 +0100
+++ b/src/HOL/Integ/NatSimprocs.thy	Wed Jan 11 10:59:55 2006 +0100
@@ -360,7 +360,7 @@
      "(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]
+lemmas half_gt_zero = half_gt_zero_iff [THEN iffD2, standard]
 declare half_gt_zero [simp]
 
 (* The following lemma should appear in Divides.thy, but there the proof
diff -r 5f5d37e763c4 -r 22f96cd085d5 src/HOL/Integ/Parity.thy
--- a/src/HOL/Integ/Parity.thy	Wed Jan 11 03:10:04 2006 +0100
+++ b/src/HOL/Integ/Parity.thy	Wed Jan 11 10:59:55 2006 +0100
@@ -348,10 +348,7 @@
 done
 
 lemma zero_less_power_nat_eq: "(0 < (x::nat) ^ n) = (n = 0 | 0 < x)"
-  apply (induct n)
-  apply simp
-  apply auto
-done
+  by (induct n, auto)
 
 lemma power_minus_even [simp]: "even n ==> 
     (- x)^n = (x^n::'a::{recpower,comm_ring_1})"
diff -r 5f5d37e763c4 -r 22f96cd085d5 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Wed Jan 11 03:10:04 2006 +0100
+++ b/src/HOL/Nat.thy	Wed Jan 11 10:59:55 2006 +0100
@@ -58,8 +58,8 @@
 
 defs
   Zero_nat_def: "0 == Abs_Nat Zero_Rep"
-  Suc_def: "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))"
-  One_nat_def [simp]: "1 == Suc 0"
+  Suc_def:      "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))"
+  One_nat_def:  "1 == Suc 0"
 
   -- {* nat operations *}
   pred_nat_def: "pred_nat == {(m, n). n = Suc m}"
@@ -68,6 +68,8 @@
 
   le_def: "m \<le> (n::nat) == ~ (n < m)"
 
+declare One_nat_def [simp]
+
 
 text {* Induction *}