# HG changeset patch
# User wenzelm
# Date 1147821821 -7200
# Node ID 2e4a143c73c5de431e17d97c0c6bbacb0e8e86a9
# Parent  95ac857276e1e45b6b882fa2e225c7be652c988b
prefer 'definition' over low-level defs;
tuned source/document;

diff -r 95ac857276e1 -r 2e4a143c73c5 src/HOL/NumberTheory/BijectionRel.thy
--- a/src/HOL/NumberTheory/BijectionRel.thy	Wed May 17 01:23:40 2006 +0200
+++ b/src/HOL/NumberTheory/BijectionRel.thy	Wed May 17 01:23:41 2006 +0200
@@ -29,15 +29,15 @@
   (and similar for @{term A}).
 *}
 
-constdefs
+definition
   bijP :: "('a => 'a => bool) => 'a set => bool"
-  "bijP P F == \<forall>a b. a \<in> F \<and> P a b --> b \<in> F"
+  "bijP P F = (\<forall>a b. a \<in> F \<and> P a b --> b \<in> F)"
 
   uniqP :: "('a => 'a => bool) => bool"
-  "uniqP P == \<forall>a b c d. P a b \<and> P c d --> (a = c) = (b = d)"
+  "uniqP P = (\<forall>a b c d. P a b \<and> P c d --> (a = c) = (b = d))"
 
   symP :: "('a => 'a => bool) => bool"
-  "symP P == \<forall>a b. P a b = P b a"
+  "symP P = (\<forall>a b. P a b = P b a)"
 
 consts
   bijER :: "('a => 'a => bool) => 'a set set"
diff -r 95ac857276e1 -r 2e4a143c73c5 src/HOL/NumberTheory/Chinese.thy
--- a/src/HOL/NumberTheory/Chinese.thy	Wed May 17 01:23:40 2006 +0200
+++ b/src/HOL/NumberTheory/Chinese.thy	Wed May 17 01:23:41 2006 +0200
@@ -31,43 +31,34 @@
   "funsum f i 0 = f i"
   "funsum f i (Suc n) = f (Suc (i + n)) + funsum f i n"
 
-consts
+definition
   m_cond :: "nat => (nat => int) => bool"
+  "m_cond n mf =
+    ((\<forall>i. i \<le> n --> 0 < mf i) \<and>
+      (\<forall>i j. i \<le> n \<and> j \<le> n \<and> i \<noteq> j --> zgcd (mf i, mf j) = 1))"
+
   km_cond :: "nat => (nat => int) => (nat => int) => bool"
+  "km_cond n kf mf = (\<forall>i. i \<le> n --> zgcd (kf i, mf i) = 1)"
+
   lincong_sol ::
     "nat => (nat => int) => (nat => int) => (nat => int) => int => bool"
+  "lincong_sol n kf bf mf x = (\<forall>i. i \<le> n --> zcong (kf i * x) (bf i) (mf i))"
 
   mhf :: "(nat => int) => nat => nat => int"
+  "mhf mf n i =
+    (if i = 0 then funprod mf (Suc 0) (n - Suc 0)
+     else if i = n then funprod mf 0 (n - Suc 0)
+     else funprod mf 0 (i - Suc 0) * funprod mf (Suc i) (n - Suc 0 - i))"
+
   xilin_sol ::
     "nat => nat => (nat => int) => (nat => int) => (nat => int) => int"
-  x_sol :: "nat => (nat => int) => (nat => int) => (nat => int) => int"
-
-defs
-  m_cond_def:
-    "m_cond n mf ==
-      (\<forall>i. i \<le> n --> 0 < mf i) \<and>
-      (\<forall>i j. i \<le> n \<and> j \<le> n \<and> i \<noteq> j --> zgcd (mf i, mf j) = 1)"
-
-  km_cond_def:
-    "km_cond n kf mf == \<forall>i. i \<le> n --> zgcd (kf i, mf i) = 1"
-
-  lincong_sol_def:
-    "lincong_sol n kf bf mf x == \<forall>i. i \<le> n --> zcong (kf i * x) (bf i) (mf i)"
+  "xilin_sol i n kf bf mf =
+    (if 0 < n \<and> i \<le> n \<and> m_cond n mf \<and> km_cond n kf mf then
+        (SOME x. 0 \<le> x \<and> x < mf i \<and> zcong (kf i * mhf mf n i * x) (bf i) (mf i))
+     else 0)"
 
-  mhf_def:
-    "mhf mf n i ==
-      if i = 0 then funprod mf (Suc 0) (n - Suc 0)
-      else if i = n then funprod mf 0 (n - Suc 0)
-      else funprod mf 0 (i - Suc 0) * funprod mf (Suc i) (n - Suc 0 - i)"
-
-  xilin_sol_def:
-    "xilin_sol i n kf bf mf ==
-      if 0 < n \<and> i \<le> n \<and> m_cond n mf \<and> km_cond n kf mf then
-        (SOME x. 0 \<le> x \<and> x < mf i \<and> zcong (kf i * mhf mf n i * x) (bf i) (mf i))
-      else 0"
-
-  x_sol_def:
-    "x_sol n kf bf mf == funsum (\<lambda>i. xilin_sol i n kf bf mf * mhf mf n i) 0 n"
+  x_sol :: "nat => (nat => int) => (nat => int) => (nat => int) => int"
+  "x_sol n kf bf mf = funsum (\<lambda>i. xilin_sol i n kf bf mf * mhf mf n i) 0 n"
 
 
 text {* \medskip @{term funprod} and @{term funsum} *}
diff -r 95ac857276e1 -r 2e4a143c73c5 src/HOL/NumberTheory/Euler.thy
--- a/src/HOL/NumberTheory/Euler.thy	Wed May 17 01:23:40 2006 +0200
+++ b/src/HOL/NumberTheory/Euler.thy	Wed May 17 01:23:41 2006 +0200
@@ -7,22 +7,20 @@
 
 theory Euler imports Residues EvenOdd begin
 
-constdefs
+definition
   MultInvPair :: "int => int => int => int set"
-  "MultInvPair a p j == {StandardRes p j, StandardRes p (a * (MultInv p j))}"
+  "MultInvPair a p j = {StandardRes p j, StandardRes p (a * (MultInv p j))}"
+
   SetS        :: "int => int => int set set"
-  "SetS        a p   ==  ((MultInvPair a p) ` (SRStar p))"
+  "SetS        a p   =  (MultInvPair a p ` SRStar p)"
 
-(****************************************************************)
-(*                                                              *)
-(* Property for MultInvPair                                     *)
-(*                                                              *)
-(****************************************************************)
+
+subsection {* Property for MultInvPair *}
 
-lemma MultInvPair_prop1a: "[| zprime p; 2 < p; ~([a = 0](mod p));
-                              X \<in> (SetS a p); Y \<in> (SetS a p);
-                              ~((X \<inter> Y) = {}) |] ==> 
-                           X = Y"
+lemma MultInvPair_prop1a:
+  "[| zprime p; 2 < p; ~([a = 0](mod p));
+      X \<in> (SetS a p); Y \<in> (SetS a p);
+      ~((X \<inter> Y) = {}) |] ==> X = Y"
   apply (auto simp add: SetS_def)
   apply (drule StandardRes_SRStar_prop1a)+ defer 1
   apply (drule StandardRes_SRStar_prop1a)+
@@ -35,16 +33,16 @@
   apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)
   apply (drule MultInv_zcong_prop2, auto simp add: zcong_sym)
   apply (drule MultInv_zcong_prop3, auto simp add: zcong_sym)
-done
+  done
 
-lemma MultInvPair_prop1b: "[| zprime p; 2 < p; ~([a = 0](mod p));
-                              X \<in> (SetS a p); Y \<in> (SetS a p);
-                              X \<noteq> Y |] ==>
-                              X \<inter> Y = {}"
+lemma MultInvPair_prop1b:
+  "[| zprime p; 2 < p; ~([a = 0](mod p));
+      X \<in> (SetS a p); Y \<in> (SetS a p);
+      X \<noteq> Y |] ==> X \<inter> Y = {}"
   apply (rule notnotD)
   apply (rule notI)
   apply (drule MultInvPair_prop1a, auto)
-done
+  done
 
 lemma MultInvPair_prop1c: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==>  
     \<forall>X \<in> SetS a p. \<forall>Y \<in> SetS a p. X \<noteq> Y --> X\<inter>Y = {}"
@@ -56,7 +54,7 @@
     SRStar_mult_prop2)
   apply (frule StandardRes_SRStar_prop3)
   apply (rule bexI, auto)
-done
+  done
 
 lemma MultInvPair_distinct: "[| zprime p; 2 < p; ~([a = 0] (mod p)); 
                                 ~([j = 0] (mod p)); 
@@ -97,11 +95,8 @@
   apply (drule MultInvPair_distinct)
 by auto
 
-(****************************************************************)
-(*                                                              *)
-(* Properties of SetS                                           *)
-(*                                                              *)
-(****************************************************************)
+
+subsection {* Properties of SetS *}
 
 lemma SetS_finite: "2 < p ==> finite (SetS a p)"
   by (auto simp add: SetS_def SRStar_finite [of p] finite_imageI)
@@ -115,7 +110,7 @@
   apply (auto simp add: SetS_def)
   apply (frule StandardRes_SRStar_prop1a)
   apply (rule MultInvPair_card_two, auto)
-done
+  done
 
 lemma Union_SetS_finite: "2 < p ==> finite (Union (SetS a p))"
   by (auto simp add: SetS_finite SetS_elems_finite finite_Union)
@@ -136,10 +131,9 @@
       by (auto simp add: prems SetS_finite SetS_elems_finite
                          MultInvPair_prop1c [of p a] card_Union_disjoint)
     also have "... = int(setsum (%x.2) (SetS a p))"
-      apply (insert prems)
-      apply (auto simp add: SetS_elems_card SetS_finite SetS_elems_finite 
+      using prems
+      by (auto simp add: SetS_elems_card SetS_finite SetS_elems_finite 
         card_setsum_aux simp del: setsum_constant)
-    done
     also have "... = 2 * int(card( SetS a p))"
       by (auto simp add: prems SetS_finite setsum_const2)
     finally show ?thesis .
@@ -164,7 +158,7 @@
   apply (frule_tac p = p and x = x in MultInv_prop2, auto)
   apply (drule_tac a = "x * MultInv p x" and b = 1 in zcong_zmult_prop2)
   apply (auto simp add: zmult_ac)
-done
+  done
 
 lemma aux1: "[| 0 < x; (x::int) < a; x \<noteq> (a - 1) |] ==> x < a - 1"
   by arith
@@ -237,13 +231,7 @@
   apply (auto simp add: Union_SetS_setprod_prop2)
   done
 
-(****************************************************************)
-(*                                                              *)
-(*  Prove the first part of Euler's Criterion:                  *)
-(*    ~(QuadRes p x) |] ==>                                     *)
-(*                   [x^(nat (((p) - 1) div 2)) = -1](mod p)    *)
-(*                                                              *)
-(****************************************************************)
+text {* \medskip Prove the first part of Euler's Criterion: *}
 
 lemma Euler_part1: "[| 2 < p; zprime p; ~([x = 0](mod p)); 
     ~(QuadRes p x) |] ==> 
@@ -254,12 +242,7 @@
   apply (rule zcong_trans, auto)
   done
 
-(********************************************************************)
-(*                                                                  *)
-(* Prove another part of Euler Criterion:                           *)
-(*        [a = 0] (mod p) ==> [0 = a ^ nat ((p - 1) div 2)] (mod p) *)
-(*                                                                  *)
-(********************************************************************)
+text {* \medskip Prove another part of Euler Criterion: *}
 
 lemma aux_1: "0 < p ==> (a::int) ^ nat (p) = a * a ^ (nat (p) - 1)"
 proof -
@@ -289,20 +272,15 @@
   then show ?thesis by auto
 qed
 
-lemma Euler_part2: "[| 2 < p; zprime p; [a = 0] (mod p) |] ==> [0 = a ^ nat ((p - 1) div 2)] (mod p)"
+lemma Euler_part2:
+    "[| 2 < p; zprime p; [a = 0] (mod p) |] ==> [0 = a ^ nat ((p - 1) div 2)] (mod p)"
   apply (frule zprime_zOdd_eq_grt_2)
   apply (frule aux_2, auto)
   apply (frule_tac a = a in aux_1, auto)
   apply (frule zcong_zmult_prop1, auto)
   done
 
-(****************************************************************)
-(*                                                              *)
-(* Prove the final part of Euler's Criterion:                   *)
-(*           QuadRes p x |] ==>                                 *)
-(*                      [x^(nat (((p) - 1) div 2)) = 1](mod p)  *)
-(*                                                              *)
-(****************************************************************)
+text {* \medskip Prove the final part of Euler's Criterion: *}
 
 lemma aux__1: "[| ~([x = 0] (mod p)); [y ^ 2 = x] (mod p)|] ==> ~(p dvd y)"
   apply (subgoal_tac "[| ~([x = 0] (mod p)); [y ^ 2 = x] (mod p)|] ==> 
@@ -329,11 +307,8 @@
   apply (auto intro: Little_Fermat simp add: zprime_zOdd_eq_grt_2)
   done
 
-(********************************************************************)
-(*                                                                  *)
-(* Finally show Euler's Criterion                                   *)
-(*                                                                  *)
-(********************************************************************)
+
+text {* \medskip Finally show Euler's Criterion: *}
 
 theorem Euler_Criterion: "[| 2 < p; zprime p |] ==> [(Legendre a p) =
     a^(nat (((p) - 1) div 2))] (mod p)"
diff -r 95ac857276e1 -r 2e4a143c73c5 src/HOL/NumberTheory/EulerFermat.thy
--- a/src/HOL/NumberTheory/EulerFermat.thy	Wed May 17 01:23:40 2006 +0200
+++ b/src/HOL/NumberTheory/EulerFermat.thy	Wed May 17 01:23:41 2006 +0200
@@ -19,12 +19,6 @@
 
 consts
   RsetR :: "int => int set set"
-  BnorRset :: "int * int => int set"
-  norRRset :: "int => int set"
-  noXRRset :: "int => int => int set"
-  phi :: "int => nat"
-  is_RRset :: "int set => int => bool"
-  RRset2norRR :: "int set => int => int => int"
 
 inductive "RsetR m"
   intros
@@ -32,6 +26,9 @@
     insert: "A \<in> RsetR m ==> zgcd (a, m) = 1 ==>
       \<forall>a'. a' \<in> A --> \<not> zcong a a' m ==> insert a A \<in> RsetR m"
 
+consts
+  BnorRset :: "int * int => int set"
+
 recdef BnorRset
   "measure ((\<lambda>(a, m). nat a) :: int * int => nat)"
   "BnorRset (a, m) =
@@ -40,20 +37,27 @@
     in (if zgcd (a, m) = 1 then insert a na else na)
     else {})"
 
-defs
-  norRRset_def: "norRRset m == BnorRset (m - 1, m)"
-  noXRRset_def: "noXRRset m x == (\<lambda>a. a * x) ` norRRset m"
-  phi_def: "phi m == card (norRRset m)"
-  is_RRset_def: "is_RRset A m == A \<in> RsetR m \<and> card A = phi m"
-  RRset2norRR_def:
-    "RRset2norRR A m a ==
+definition
+  norRRset :: "int => int set"
+  "norRRset m = BnorRset (m - 1, m)"
+
+  noXRRset :: "int => int => int set"
+  "noXRRset m x = (\<lambda>a. a * x) ` norRRset m"
+
+  phi :: "int => nat"
+  "phi m = card (norRRset m)"
+
+  is_RRset :: "int set => int => bool"
+  "is_RRset A m = (A \<in> RsetR m \<and> card A = phi m)"
+
+  RRset2norRR :: "int set => int => int => int"
+  "RRset2norRR A m a =
      (if 1 < m \<and> is_RRset A m \<and> a \<in> A then
         SOME b. zcong a b m \<and> b \<in> norRRset m
       else 0)"
 
-constdefs
   zcongm :: "int => int => int => bool"
-  "zcongm m == \<lambda>a b. zcong a b m"
+  "zcongm m = (\<lambda>a b. zcong a b m)"
 
 lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \<or> z = -1)"
   -- {* LCP: not sure why this lemma is needed now *}
diff -r 95ac857276e1 -r 2e4a143c73c5 src/HOL/NumberTheory/EvenOdd.thy
--- a/src/HOL/NumberTheory/EvenOdd.thy	Wed May 17 01:23:40 2006 +0200
+++ b/src/HOL/NumberTheory/EvenOdd.thy	Wed May 17 01:23:41 2006 +0200
@@ -7,20 +7,13 @@
 
 theory EvenOdd imports Int2 begin
 
-text{*Note.  This theory is being revised.  See the web page
-\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
-
-constdefs
+definition
   zOdd    :: "int set"
-  "zOdd == {x. \<exists>k. x = 2 * k + 1}"
+  "zOdd = {x. \<exists>k. x = 2 * k + 1}"
   zEven   :: "int set"
-  "zEven == {x. \<exists>k. x = 2 * k}"
+  "zEven = {x. \<exists>k. x = 2 * k}"
 
-(***********************************************************)
-(*                                                         *)
-(* Some useful properties about even and odd               *)
-(*                                                         *)
-(***********************************************************)
+subsection {* Some useful properties about even and odd *}
 
 lemma zOddI [intro?]: "x = 2 * k + 1 \<Longrightarrow> x \<in> zOdd"
   and zOddE [elim?]: "x \<in> zOdd \<Longrightarrow> (!!k. x = 2 * k + 1 \<Longrightarrow> C) \<Longrightarrow> C"
diff -r 95ac857276e1 -r 2e4a143c73c5 src/HOL/NumberTheory/Factorization.thy
--- a/src/HOL/NumberTheory/Factorization.thy	Wed May 17 01:23:40 2006 +0200
+++ b/src/HOL/NumberTheory/Factorization.thy	Wed May 17 01:23:41 2006 +0200
@@ -11,16 +11,16 @@
 
 subsection {* Definitions *}
 
+definition
+  primel :: "nat list => bool "
+  "primel xs = (\<forall>p \<in> set xs. prime p)"
+
 consts
-  primel :: "nat list => bool "
   nondec :: "nat list => bool "
   prod :: "nat list => nat"
   oinsert :: "nat => nat list => nat list"
   sort :: "nat list => nat list"
 
-defs
-  primel_def: "primel xs == \<forall>p \<in> set xs. prime p"
-
 primrec
   "nondec [] = True"
   "nondec (x # xs) = (case xs of [] => True | y # ys => x \<le> y \<and> nondec xs)"
@@ -41,12 +41,12 @@
 subsection {* Arithmetic *}
 
 lemma one_less_m: "(m::nat) \<noteq> m * k ==> m \<noteq> Suc 0 ==> Suc 0 < m"
-  apply (case_tac m)
+  apply (cases m)
    apply auto
   done
 
 lemma one_less_k: "(m::nat) \<noteq> m * k ==> Suc 0 < m * k ==> Suc 0 < k"
-  apply (case_tac k)
+  apply (cases k)
    apply auto
   done
 
@@ -55,7 +55,7 @@
   done
 
 lemma mn_eq_m_one: "(0::nat) < m ==> m * n = m ==> n = Suc 0"
-  apply (case_tac n)
+  apply (cases n)
    apply auto
   done
 
@@ -116,9 +116,8 @@
   done
 
 lemma primel_one_empty: "primel xs ==> prod xs = Suc 0 ==> xs = []"
-  apply (unfold primel_def prime_def)
-  apply (case_tac xs)
-   apply simp_all
+  apply (cases xs)
+   apply (simp_all add: primel_def prime_def)
   done
 
 lemma prime_g_one: "prime p ==> Suc 0 < p"
@@ -131,25 +130,25 @@
   apply auto
   done
 
-lemma primel_nempty_g_one [rule_format]:
-    "primel xs --> xs \<noteq> [] --> Suc 0 < prod xs"
-  apply (unfold primel_def prime_def)
+lemma primel_nempty_g_one:
+    "primel xs \<Longrightarrow> xs \<noteq> [] \<Longrightarrow> Suc 0 < prod xs"
   apply (induct xs)
-   apply (auto elim: one_less_mult)
+   apply simp
+  apply (fastsimp simp: primel_def prime_def elim: one_less_mult)
   done
 
 lemma primel_prod_gz: "primel xs ==> 0 < prod xs"
-  apply (unfold primel_def prime_def)
   apply (induct xs)
-   apply auto
+   apply (auto simp: primel_def prime_def)
   done
 
 
 subsection {* Sorting *}
 
-lemma nondec_oinsert [rule_format]: "nondec xs --> nondec (oinsert x xs)"
+lemma nondec_oinsert: "nondec xs \<Longrightarrow> nondec (oinsert x xs)"
   apply (induct xs)
-   apply (case_tac [2] xs)
+   apply simp
+   apply (case_tac xs)
     apply (simp_all cong del: list.weak_case_cong)
   done
 
@@ -163,7 +162,7 @@
   apply simp_all
   done
 
-lemma nondec_sort_eq [rule_format]: "nondec xs --> xs = sort xs"
+lemma nondec_sort_eq [rule_format]: "nondec xs \<longrightarrow> xs = sort xs"
   apply (induct xs)
    apply safe
     apply simp_all
@@ -185,7 +184,7 @@
 
 lemma perm_primel [rule_format]: "xs <~~> ys ==> primel xs --> primel ys"
   apply (unfold primel_def)
-  apply (erule perm.induct)
+  apply (induct set: perm)
      apply simp
     apply simp
    apply (simp (no_asm))
@@ -193,13 +192,13 @@
   apply blast
   done
 
-lemma perm_prod [rule_format]: "xs <~~> ys ==> prod xs = prod ys"
-  apply (erule perm.induct)
+lemma perm_prod: "xs <~~> ys ==> prod xs = prod ys"
+  apply (induct set: perm)
      apply (simp_all add: mult_ac)
   done
 
 lemma perm_subst_oinsert: "xs <~~> ys ==> oinsert a xs <~~> oinsert a ys"
-  apply (erule perm.induct)
+  apply (induct set: perm)
      apply auto
   done
 
@@ -214,7 +213,7 @@
   done
 
 lemma perm_sort_eq: "xs <~~> ys ==> sort xs = sort ys"
-  apply (erule perm.induct)
+  apply (induct set: perm)
      apply (simp_all add: oinsert_x_y)
   done
 
diff -r 95ac857276e1 -r 2e4a143c73c5 src/HOL/NumberTheory/Finite2.thy
--- a/src/HOL/NumberTheory/Finite2.thy	Wed May 17 01:23:40 2006 +0200
+++ b/src/HOL/NumberTheory/Finite2.thy	Wed May 17 01:23:41 2006 +0200
@@ -9,23 +9,17 @@
 imports IntFact
 begin
 
-text{*These are useful for combinatorial and number-theoretic counting
-arguments.*}
-
-text{*Note.  This theory is being revised.  See the web page
-\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
+text{*
+  These are useful for combinatorial and number-theoretic counting
+  arguments.
+*}
 
-(******************************************************************)
-(*                                                                *)
-(* Useful properties of sums and products                         *)
-(*                                                                *)
-(******************************************************************)
 
 subsection {* Useful properties of sums and products *}
 
 lemma setsum_same_function_zcong:
-assumes a: "\<forall>x \<in> S. [f x = g x](mod m)"
-shows "[setsum f S = setsum g S] (mod m)"
+  assumes a: "\<forall>x \<in> S. [f x = g x](mod m)"
+  shows "[setsum f S = setsum g S] (mod m)"
 proof cases
   assume "finite S"
   thus ?thesis using a by induct (simp_all add: zcong_zadd)
@@ -34,8 +28,8 @@
 qed
 
 lemma setprod_same_function_zcong:
-assumes a: "\<forall>x \<in> S. [f x = g x](mod m)"
-shows "[setprod f S = setprod g S] (mod m)"
+  assumes a: "\<forall>x \<in> S. [f x = g x](mod m)"
+  shows "[setprod f S = setprod g S] (mod m)"
 proof cases
   assume "finite S"
   thus ?thesis using a by induct (simp_all add: zcong_zmult)
@@ -59,12 +53,6 @@
   by (induct set: Finites) (auto simp add: zadd_zmult_distrib2)
 
 
-(******************************************************************)
-(*                                                                *)
-(* Cardinality of some explicit finite sets                       *)
-(*                                                                *)
-(******************************************************************)
-
 subsection {* Cardinality of explicit finite sets *}
 
 lemma finite_surjI: "[| B \<subseteq> f ` A; finite A |] ==> finite B"
@@ -80,19 +68,19 @@
 qed
 
 lemma  bdd_int_set_l_finite: "finite {x::int. 0 \<le> x & x < n}"
-apply (subgoal_tac " {(x :: int). 0 \<le> x & x < n} \<subseteq>
-    int ` {(x :: nat). x < nat n}")
-apply (erule finite_surjI)
-apply (auto simp add: bdd_nat_set_l_finite image_def)
-apply (rule_tac x = "nat x" in exI, simp)
-done
+  apply (subgoal_tac " {(x :: int). 0 \<le> x & x < n} \<subseteq>
+      int ` {(x :: nat). x < nat n}")
+   apply (erule finite_surjI)
+   apply (auto simp add: bdd_nat_set_l_finite image_def)
+  apply (rule_tac x = "nat x" in exI, simp)
+  done
 
 lemma bdd_int_set_le_finite: "finite {x::int. 0 \<le> x & x \<le> n}"
-apply (subgoal_tac "{x. 0 \<le> x & x \<le> n} = {x. 0 \<le> x & x < n + 1}")
-apply (erule ssubst)
-apply (rule bdd_int_set_l_finite)
-apply auto
-done
+  apply (subgoal_tac "{x. 0 \<le> x & x \<le> n} = {x. 0 \<le> x & x < n + 1}")
+   apply (erule ssubst)
+   apply (rule bdd_int_set_l_finite)
+  apply auto
+  done
 
 lemma bdd_int_set_l_l_finite: "finite {x::int. 0 < x & x < n}"
 proof -
@@ -192,7 +180,7 @@
     int(card {x. 0 < x & x < n}) = n - 1"
   apply (auto simp add: card_bdd_int_set_l_l)
   apply (subgoal_tac "Suc 0 \<le> nat n")
-  apply (auto simp add: zdiff_int [symmetric])
+   apply (auto simp add: zdiff_int [symmetric])
   apply (subgoal_tac "0 < nat n", arith)
   apply (simp add: zero_less_nat_eq)
   done
@@ -201,11 +189,6 @@
     int(card {x. 0 < x & x \<le> n}) = n"
   by (auto simp add: card_bdd_int_set_l_le)
 
-(******************************************************************)
-(*                                                                *)
-(* Cartesian products of finite sets                              *)
-(*                                                                *)
-(******************************************************************)
 
 subsection {* Cardinality of finite cartesian products *}
 
@@ -214,35 +197,29 @@
   by blast
  *)
 
-(******************************************************************)
-(*                                                                *)
-(* Sums and products over finite sets                             *)
-(*                                                                *)
-(******************************************************************)
-
-subsection {* Lemmas for counting arguments *}
+text {* Lemmas for counting arguments. *}
 
 lemma setsum_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A;
     g ` B \<subseteq> A; inj_on g B |] ==> setsum g B = setsum (g \<circ> f) A"
-apply (frule_tac h = g and f = f in setsum_reindex)
-apply (subgoal_tac "setsum g B = setsum g (f ` A)")
-apply (simp add: inj_on_def)
-apply (subgoal_tac "card A = card B")
-apply (drule_tac A = "f ` A" and B = B in card_seteq)
-apply (auto simp add: card_image)
-apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
-apply (frule_tac A = B and B = A and f = g in card_inj_on_le)
-apply auto
-done
+  apply (frule_tac h = g and f = f in setsum_reindex)
+  apply (subgoal_tac "setsum g B = setsum g (f ` A)")
+   apply (simp add: inj_on_def)
+  apply (subgoal_tac "card A = card B")
+   apply (drule_tac A = "f ` A" and B = B in card_seteq)
+     apply (auto simp add: card_image)
+  apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
+  apply (frule_tac A = B and B = A and f = g in card_inj_on_le)
+    apply auto
+  done
 
 lemma setprod_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A;
     g ` B \<subseteq> A; inj_on g B |] ==> setprod g B = setprod (g \<circ> f) A"
   apply (frule_tac h = g and f = f in setprod_reindex)
   apply (subgoal_tac "setprod g B = setprod g (f ` A)")
-  apply (simp add: inj_on_def)
+   apply (simp add: inj_on_def)
   apply (subgoal_tac "card A = card B")
-  apply (drule_tac A = "f ` A" and B = B in card_seteq)
-  apply (auto simp add: card_image)
+   apply (drule_tac A = "f ` A" and B = B in card_seteq)
+     apply (auto simp add: card_image)
   apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
   apply (frule_tac A = B and B = A and f = g in card_inj_on_le, auto)
   done
diff -r 95ac857276e1 -r 2e4a143c73c5 src/HOL/NumberTheory/Int2.thy
--- a/src/HOL/NumberTheory/Int2.thy	Wed May 17 01:23:40 2006 +0200
+++ b/src/HOL/NumberTheory/Int2.thy	Wed May 17 01:23:41 2006 +0200
@@ -7,18 +7,12 @@
 
 theory Int2 imports Finite2 WilsonRuss begin
 
-text{*Note.  This theory is being revised.  See the web page
-\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
+definition
+  MultInv :: "int => int => int"
+  "MultInv p x = x ^ nat (p - 2)"
 
-constdefs
-  MultInv :: "int => int => int" 
-  "MultInv p x == x ^ nat (p - 2)"
 
-(*****************************************************************)
-(*                                                               *)
-(* Useful lemmas about dvd and powers                            *)
-(*                                                               *)
-(*****************************************************************)
+subsection {* Useful lemmas about dvd and powers *}
 
 lemma zpower_zdvd_prop1:
   "0 < n \<Longrightarrow> p dvd y \<Longrightarrow> p dvd ((y::int) ^ n)"
@@ -32,7 +26,7 @@
   then show ?thesis by auto
 qed
 
-lemma zprime_zdvd_zmult_better: "[| zprime p;  p dvd (m * n) |] ==> 
+lemma zprime_zdvd_zmult_better: "[| zprime p;  p dvd (m * n) |] ==>
     (p dvd m) | (p dvd n)"
   apply (cases "0 \<le> m")
   apply (simp add: zprime_zdvd_zmult)
@@ -83,11 +77,8 @@
     by arith
 qed
 
-(*****************************************************************)
-(*                                                               *)
-(* Useful properties of congruences                              *)
-(*                                                               *)
-(*****************************************************************)
+
+subsection {* Useful properties of congruences *}
 
 lemma zcong_eq_zdvd_prop: "[x = 0](mod p) = (p dvd x)"
   by (auto simp add: zcong_def)
@@ -101,7 +92,7 @@
 lemma zcong_zpower: "[x = y](mod m) ==> [x^z = y^z](mod m)"
   by (induct z) (auto simp add: zcong_zmult)
 
-lemma zcong_eq_trans: "[| [a = b](mod m); b = c; [c = d](mod m) |] ==> 
+lemma zcong_eq_trans: "[| [a = b](mod m); b = c; [c = d](mod m) |] ==>
     [a = d](mod m)"
   apply (erule zcong_trans)
   apply simp
@@ -110,7 +101,7 @@
 lemma aux1: "a - b = (c::int) ==> a = c + b"
   by auto
 
-lemma zcong_zmult_prop1: "[a = b](mod m) ==> ([c = a * d](mod m) = 
+lemma zcong_zmult_prop1: "[a = b](mod m) ==> ([c = a * d](mod m) =
     [c = b * d] (mod m))"
   apply (auto simp add: zcong_def dvd_def)
   apply (rule_tac x = "ka + k * d" in exI)
@@ -121,17 +112,17 @@
   apply (auto simp add: int_distrib)
   done
 
-lemma zcong_zmult_prop2: "[a = b](mod m) ==> 
+lemma zcong_zmult_prop2: "[a = b](mod m) ==>
     ([c = d * a](mod m) = [c = d * b] (mod m))"
   by (auto simp add: zmult_ac zcong_zmult_prop1)
 
-lemma zcong_zmult_prop3: "[| zprime p; ~[x = 0] (mod p); 
+lemma zcong_zmult_prop3: "[| zprime p; ~[x = 0] (mod p);
     ~[y = 0] (mod p) |] ==> ~[x * y = 0] (mod p)"
   apply (auto simp add: zcong_def)
   apply (drule zprime_zdvd_zmult_better, auto)
   done
 
-lemma zcong_less_eq: "[| 0 < x; 0 < y; 0 < m; [x = y] (mod m); 
+lemma zcong_less_eq: "[| 0 < x; 0 < y; 0 < m; [x = y] (mod m);
     x < m; y < m |] ==> x = y"
   apply (simp add: zcong_zmod_eq)
   apply (subgoal_tac "(x mod m) = x")
@@ -141,7 +132,7 @@
   apply auto
   done
 
-lemma zcong_neg_1_impl_ne_1: "[| 2 < p; [x = -1] (mod p) |] ==> 
+lemma zcong_neg_1_impl_ne_1: "[| 2 < p; [x = -1] (mod p) |] ==>
     ~([x = 1] (mod p))"
 proof
   assume "2 < p" and "[x = 1] (mod p)" and "[x = -1] (mod p)"
@@ -162,18 +153,18 @@
 lemma zcong_zero_equiv_div: "[a = 0] (mod m) = (m dvd a)"
   by (auto simp add: zcong_def)
 
-lemma zcong_zprime_prod_zero: "[| zprime p; 0 < a |] ==> 
-    [a * b = 0] (mod p) ==> [a = 0] (mod p) | [b = 0] (mod p)" 
+lemma zcong_zprime_prod_zero: "[| zprime p; 0 < a |] ==>
+    [a * b = 0] (mod p) ==> [a = 0] (mod p) | [b = 0] (mod p)"
   by (auto simp add: zcong_zero_equiv_div zprime_zdvd_zmult)
 
 lemma zcong_zprime_prod_zero_contra: "[| zprime p; 0 < a |] ==>
   ~[a = 0](mod p) & ~[b = 0](mod p) ==> ~[a * b = 0] (mod p)"
-  apply auto 
+  apply auto
   apply (frule_tac a = a and b = b and p = p in zcong_zprime_prod_zero)
   apply auto
   done
 
-lemma zcong_not_zero: "[| 0 < x; x < m |] ==> ~[x = 0] (mod m)" 
+lemma zcong_not_zero: "[| 0 < x; x < m |] ==> ~[x = 0] (mod m)"
   by (auto simp add: zcong_zero_equiv_div zdvd_not_zless)
 
 lemma zcong_zero: "[| 0 \<le> x; x < m; [x = 0](mod m) |] ==> x = 0"
@@ -186,17 +177,14 @@
     ==> zgcd (setprod id A,y) = 1"
   by (induct set: Finites) (auto simp add: zgcd_zgcd_zmult)
 
-(*****************************************************************)
-(*                                                               *)
-(* Some properties of MultInv                                    *)
-(*                                                               *)
-(*****************************************************************)
 
-lemma MultInv_prop1: "[| 2 < p; [x = y] (mod p) |] ==> 
+subsection {* Some properties of MultInv *}
+
+lemma MultInv_prop1: "[| 2 < p; [x = y] (mod p) |] ==>
     [(MultInv p x) = (MultInv p y)] (mod p)"
   by (auto simp add: MultInv_def zcong_zpower)
 
-lemma MultInv_prop2: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> 
+lemma MultInv_prop2: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==>
   [(x * (MultInv p x)) = 1] (mod p)"
 proof (simp add: MultInv_def zcong_eq_zdvd_prop)
   assume "2 < p" and "zprime p" and "~ p dvd x"
@@ -208,11 +196,11 @@
   finally have "[x * x ^ nat (p - 2) = x ^ nat (p - 1)] (mod p)"
     by (rule ssubst, auto)
   also from prems have "[x ^ nat (p - 1) = 1] (mod p)"
-    by (auto simp add: Little_Fermat) 
+    by (auto simp add: Little_Fermat)
   finally (zcong_trans) show "[x * x ^ nat (p - 2) = 1] (mod p)" .
 qed
 
-lemma MultInv_prop2a: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> 
+lemma MultInv_prop2a: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==>
     [(MultInv p x) * x = 1] (mod p)"
   by (auto simp add: MultInv_prop2 zmult_ac)
 
@@ -222,15 +210,15 @@
 lemma aux_2: "2 < p ==> 0 < nat (p - 2)"
   by auto
 
-lemma MultInv_prop3: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> 
+lemma MultInv_prop3: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==>
     ~([MultInv p x = 0](mod p))"
   apply (auto simp add: MultInv_def zcong_eq_zdvd_prop aux_1)
   apply (drule aux_2)
   apply (drule zpower_zdvd_prop2, auto)
   done
 
-lemma aux__1: "[| 2 < p; zprime p; ~([x = 0](mod p))|] ==> 
-    [(MultInv p (MultInv p x)) = (x * (MultInv p x) * 
+lemma aux__1: "[| 2 < p; zprime p; ~([x = 0](mod p))|] ==>
+    [(MultInv p (MultInv p x)) = (x * (MultInv p x) *
       (MultInv p (MultInv p x)))] (mod p)"
   apply (drule MultInv_prop2, auto)
   apply (drule_tac k = "MultInv p (MultInv p x)" in zcong_scalar, auto)
@@ -246,17 +234,17 @@
   apply (auto simp add: zmult_ac)
   done
 
-lemma MultInv_prop4: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==> 
+lemma MultInv_prop4: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==>
     [(MultInv p (MultInv p x)) = x] (mod p)"
   apply (frule aux__1, auto)
   apply (drule aux__2, auto)
   apply (drule zcong_trans, auto)
   done
 
-lemma MultInv_prop5: "[| 2 < p; zprime p; ~([x = 0](mod p)); 
-    ~([y = 0](mod p)); [(MultInv p x) = (MultInv p y)] (mod p) |] ==> 
+lemma MultInv_prop5: "[| 2 < p; zprime p; ~([x = 0](mod p));
+    ~([y = 0](mod p)); [(MultInv p x) = (MultInv p y)] (mod p) |] ==>
     [x = y] (mod p)"
-  apply (drule_tac a = "MultInv p x" and b = "MultInv p y" and 
+  apply (drule_tac a = "MultInv p x" and b = "MultInv p y" and
     m = p and k = x in zcong_scalar)
   apply (insert MultInv_prop2 [of p x], simp)
   apply (auto simp only: zcong_sym [of "MultInv p x * x"])
@@ -268,43 +256,43 @@
   apply (auto simp add: zcong_sym)
   done
 
-lemma MultInv_zcong_prop1: "[| 2 < p; [j = k] (mod p) |] ==> 
+lemma MultInv_zcong_prop1: "[| 2 < p; [j = k] (mod p) |] ==>
     [a * MultInv p j = a * MultInv p k] (mod p)"
   by (drule MultInv_prop1, auto simp add: zcong_scalar2)
 
-lemma aux___1: "[j = a * MultInv p k] (mod p) ==> 
+lemma aux___1: "[j = a * MultInv p k] (mod p) ==>
     [j * k = a * MultInv p k * k] (mod p)"
   by (auto simp add: zcong_scalar)
 
-lemma aux___2: "[|2 < p; zprime p; ~([k = 0](mod p)); 
+lemma aux___2: "[|2 < p; zprime p; ~([k = 0](mod p));
     [j * k = a * MultInv p k * k] (mod p) |] ==> [j * k = a] (mod p)"
-  apply (insert MultInv_prop2a [of p k] zcong_zmult_prop2 
+  apply (insert MultInv_prop2a [of p k] zcong_zmult_prop2
     [of "MultInv p k * k" 1 p "j * k" a])
   apply (auto simp add: zmult_ac)
   done
 
-lemma aux___3: "[j * k = a] (mod p) ==> [(MultInv p j) * j * k = 
+lemma aux___3: "[j * k = a] (mod p) ==> [(MultInv p j) * j * k =
      (MultInv p j) * a] (mod p)"
   by (auto simp add: zmult_assoc zcong_scalar2)
 
-lemma aux___4: "[|2 < p; zprime p; ~([j = 0](mod p)); 
+lemma aux___4: "[|2 < p; zprime p; ~([j = 0](mod p));
     [(MultInv p j) * j * k = (MultInv p j) * a] (mod p) |]
        ==> [k = a * (MultInv p j)] (mod p)"
-  apply (insert MultInv_prop2a [of p j] zcong_zmult_prop1 
+  apply (insert MultInv_prop2a [of p j] zcong_zmult_prop1
     [of "MultInv p j * j" 1 p "MultInv p j * a" k])
   apply (auto simp add: zmult_ac zcong_sym)
   done
 
-lemma MultInv_zcong_prop2: "[| 2 < p; zprime p; ~([k = 0](mod p)); 
-    ~([j = 0](mod p)); [j = a * MultInv p k] (mod p) |] ==> 
+lemma MultInv_zcong_prop2: "[| 2 < p; zprime p; ~([k = 0](mod p));
+    ~([j = 0](mod p)); [j = a * MultInv p k] (mod p) |] ==>
     [k = a * MultInv p j] (mod p)"
   apply (drule aux___1)
   apply (frule aux___2, auto)
   by (drule aux___3, drule aux___4, auto)
 
-lemma MultInv_zcong_prop3: "[| 2 < p; zprime p; ~([a = 0](mod p)); 
+lemma MultInv_zcong_prop3: "[| 2 < p; zprime p; ~([a = 0](mod p));
     ~([k = 0](mod p)); ~([j = 0](mod p));
-    [a * MultInv p j = a * MultInv p k] (mod p) |] ==> 
+    [a * MultInv p j = a * MultInv p k] (mod p) |] ==>
       [j = k] (mod p)"
   apply (auto simp add: zcong_eq_zdvd_prop [of a p])
   apply (frule zprime_imp_zrelprime, auto)
diff -r 95ac857276e1 -r 2e4a143c73c5 src/HOL/NumberTheory/IntPrimes.thy
--- a/src/HOL/NumberTheory/IntPrimes.thy	Wed May 17 01:23:40 2006 +0200
+++ b/src/HOL/NumberTheory/IntPrimes.thy	Wed May 17 01:23:41 2006 +0200
@@ -31,18 +31,18 @@
 		      s, s' - (r' div r) * s, 
 		      t, t' - (r' div r) * t))"
 
-constdefs
+definition
   zgcd :: "int * int => int"
-  "zgcd == \<lambda>(x,y). int (gcd (nat (abs x), nat (abs y)))"
+  "zgcd = (\<lambda>(x,y). int (gcd (nat (abs x), nat (abs y))))"
 
   zprime :: "int \<Rightarrow> bool"
-  "zprime p == 1 < p \<and> (\<forall>m. 0 <= m & m dvd p --> m = 1 \<or> m = p)"
+  "zprime p = (1 < p \<and> (\<forall>m. 0 <= m & m dvd p --> m = 1 \<or> m = p))"
 
   xzgcd :: "int => int => int * int * int"
-  "xzgcd m n == xzgcda (m, n, m, n, 1, 0, 0, 1)"
+  "xzgcd m n = xzgcda (m, n, m, n, 1, 0, 0, 1)"
 
   zcong :: "int => int => int => bool"    ("(1[_ = _] '(mod _'))")
-  "[a = b] (mod m) == m dvd (a - b)"
+  "[a = b] (mod m) = (m dvd (a - b))"
 
 
 
diff -r 95ac857276e1 -r 2e4a143c73c5 src/HOL/NumberTheory/Quadratic_Reciprocity.thy
--- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Wed May 17 01:23:40 2006 +0200
+++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Wed May 17 01:23:41 2006 +0200
@@ -9,12 +9,10 @@
 imports Gauss
 begin
 
-(***************************************************************)
-(*                                                             *)
-(*  Lemmas leading up to the proof of theorem 3.3 in           *)
-(*  Niven and Zuckerman's presentation                         *)
-(*                                                             *)
-(***************************************************************)
+text {*
+  Lemmas leading up to the proof of theorem 3.3 in Niven and
+  Zuckerman's presentation.
+*}
 
 lemma (in GAUSS) QRLemma1: "a * setsum id A =
   p * setsum (%x. ((x * a) div p)) A + setsum id D + setsum id E"
@@ -149,11 +147,8 @@
   apply (auto simp add: GAUSS_def)
   done
 
-(******************************************************************)
-(*                                                                *)
-(* Stuff about S, S1 and S2...                                    *)
-(*                                                                *)
-(******************************************************************)
+
+subsection {* Stuff about S, S1 and S2 *}
 
 locale QRTEMP =
   fixes p     :: "int"
diff -r 95ac857276e1 -r 2e4a143c73c5 src/HOL/NumberTheory/Residues.thy
--- a/src/HOL/NumberTheory/Residues.thy	Wed May 17 01:23:40 2006 +0200
+++ b/src/HOL/NumberTheory/Residues.thy	Wed May 17 01:23:41 2006 +0200
@@ -7,45 +7,33 @@
 
 theory Residues imports Int2 begin
 
-text{*Note.  This theory is being revised.  See the web page
-\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
+text {*
+  \medskip Define the residue of a set, the standard residue,
+  quadratic residues, and prove some basic properties. *}
 
-(*****************************************************************)
-(*                                                               *)
-(* Define the residue of a set, the standard residue, quadratic  *)
-(* residues, and prove some basic properties.                    *)
-(*                                                               *)
-(*****************************************************************)
-
-constdefs
+definition
   ResSet      :: "int => int set => bool"
-  "ResSet m X == \<forall>y1 y2. (((y1 \<in> X) & (y2 \<in> X) & [y1 = y2] (mod m)) --> 
-    y1 = y2)"
+  "ResSet m X = (\<forall>y1 y2. (y1 \<in> X & y2 \<in> X & [y1 = y2] (mod m) --> y1 = y2))"
 
   StandardRes :: "int => int => int"
-  "StandardRes m x == x mod m"
+  "StandardRes m x = x mod m"
 
   QuadRes     :: "int => int => bool"
-  "QuadRes m x == \<exists>y. ([(y ^ 2) = x] (mod m))"
+  "QuadRes m x = (\<exists>y. ([(y ^ 2) = x] (mod m)))"
 
   Legendre    :: "int => int => int"      
-  "Legendre a p == (if ([a = 0] (mod p)) then 0
+  "Legendre a p = (if ([a = 0] (mod p)) then 0
                      else if (QuadRes p a) then 1
                      else -1)"
 
   SR          :: "int => int set"
-  "SR p == {x. (0 \<le> x) & (x < p)}"
+  "SR p = {x. (0 \<le> x) & (x < p)}"
 
   SRStar      :: "int => int set"
-  "SRStar p == {x. (0 < x) & (x < p)}"
+  "SRStar p = {x. (0 < x) & (x < p)}"
 
-(******************************************************************)
-(*                                                                *)
-(* Some useful properties of StandardRes                          *)
-(*                                                                *)
-(******************************************************************)
 
-subsection {* Properties of StandardRes *}
+subsection {* Some useful properties of StandardRes *}
 
 lemma StandardRes_prop1: "[x = StandardRes m x] (mod m)"
   by (auto simp add: StandardRes_def zcong_zmod)
@@ -72,11 +60,6 @@
    "(StandardRes m x = 0) = ([x = 0](mod m))"
   by (auto simp add: StandardRes_def zcong_eq_zdvd_prop dvd_def) 
 
-(******************************************************************)
-(*                                                                *)
-(* Some useful stuff relating StandardRes and SRStar and SR       *)
-(*                                                                *)
-(******************************************************************)
 
 subsection {* Relations between StandardRes, SRStar, and SR *}
 
@@ -132,11 +115,6 @@
 lemma SRStar_finite: "2 < p ==> finite( SRStar p)"
   by (auto simp add: SRStar_def bdd_int_set_l_l_finite)
 
-(******************************************************************)
-(*                                                                *)
-(* Some useful stuff about ResSet and StandardRes                 *)
-(*                                                                *)
-(******************************************************************)
 
 subsection {* Properties relating ResSets with StandardRes *}
 
@@ -175,14 +153,13 @@
   apply (auto intro!: zcong_zmult simp add: StandardRes_prop1)
   done
 
-lemma ResSet_image: "[| 0 < m; ResSet m A; \<forall>x \<in> A. \<forall>y \<in> A. ([f x = f y](mod m) --> x = y) |] ==> ResSet m (f ` A)"
+lemma ResSet_image:
+  "[| 0 < m; ResSet m A; \<forall>x \<in> A. \<forall>y \<in> A. ([f x = f y](mod m) --> x = y) |] ==>
+    ResSet m (f ` A)"
   by (auto simp add: ResSet_def)
 
-(****************************************************************)
-(*                                                              *)
-(* Property for SRStar                                          *)
-(*                                                              *)
-(****************************************************************)
+
+subsection {* Property for SRStar *}
 
 lemma ResSet_SRStar_prop: "ResSet p (SRStar p)"
   by (auto simp add: SRStar_def ResSet_def zcong_zless_imp_eq)
diff -r 95ac857276e1 -r 2e4a143c73c5 src/HOL/NumberTheory/WilsonBij.thy
--- a/src/HOL/NumberTheory/WilsonBij.thy	Wed May 17 01:23:40 2006 +0200
+++ b/src/HOL/NumberTheory/WilsonBij.thy	Wed May 17 01:23:41 2006 +0200
@@ -17,15 +17,14 @@
 
 subsection {* Definitions and lemmas *}
 
-constdefs
+definition
   reciR :: "int => int => int => bool"
-  "reciR p ==
-    \<lambda>a b. zcong (a * b) 1 p \<and> 1 < a \<and> a < p - 1 \<and> 1 < b \<and> b < p - 1"
+  "reciR p = (\<lambda>a b. zcong (a * b) 1 p \<and> 1 < a \<and> a < p - 1 \<and> 1 < b \<and> b < p - 1)"
   inv :: "int => int => int"
-  "inv p a ==
-    if zprime p \<and> 0 < a \<and> a < p then
+  "inv p a =
+    (if zprime p \<and> 0 < a \<and> a < p then
       (SOME x. 0 \<le> x \<and> x < p \<and> zcong (a * x) 1 p)
-    else 0"
+     else 0)"
 
 
 text {* \medskip Inverse *}
diff -r 95ac857276e1 -r 2e4a143c73c5 src/HOL/NumberTheory/WilsonRuss.thy
--- a/src/HOL/NumberTheory/WilsonRuss.thy	Wed May 17 01:23:40 2006 +0200
+++ b/src/HOL/NumberTheory/WilsonRuss.thy	Wed May 17 01:23:41 2006 +0200
@@ -15,13 +15,13 @@
 
 subsection {* Definitions and lemmas *}
 
+definition
+  inv :: "int => int => int"
+  "inv p a = (a^(nat (p - 2))) mod p"
+
 consts
-  inv :: "int => int => int"
   wset :: "int * int => int set"
 
-defs
-  inv_def: "inv p a == (a^(nat (p - 2))) mod p"
-
 recdef wset
   "measure ((\<lambda>(a, p). nat a) :: int * int => nat)"
   "wset (a, p) =
@@ -81,7 +81,8 @@
       apply (rule_tac [2] zcong_zless_imp_eq, auto)
   done
 
-lemma inv_not_p_minus_1_aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
+lemma inv_not_p_minus_1_aux:
+    "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
   apply (unfold zcong_def)
   apply (simp add: OrderedGroup.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
   apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
@@ -163,7 +164,8 @@
 
 lemma wset_induct:
   assumes "!!a p. P {} a p"
-    and "!!a p. 1 < (a::int) \<Longrightarrow> P (wset (a - 1, p)) (a - 1) p ==> P (wset (a, p)) a p"
+    and "!!a p. 1 < (a::int) \<Longrightarrow>
+      P (wset (a - 1, p)) (a - 1) p ==> P (wset (a, p)) a p"
   shows "P (wset (u, v)) u v"
   apply (rule wset.induct, safe)
    prefer 2