# HG changeset patch
# User wenzelm
# Date 1281091020 -7200
# Node ID e9b4835a54ee864999a2c8eaf8055d15d37344e6
# Parent  8aaa21db41f3e4549be08540bae2547c355d72a1
modernized specifications;
tuned headers;

diff -r 8aaa21db41f3 -r e9b4835a54ee src/HOL/Old_Number_Theory/BijectionRel.thy
--- a/src/HOL/Old_Number_Theory/BijectionRel.thy	Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/BijectionRel.thy	Fri Aug 06 12:37:00 2010 +0200
@@ -1,10 +1,13 @@
-(*  Author:     Thomas M. Rasmussen
+(*  Title:      HOL/Old_Number_Theory/BijectionRel.thy
+    Author:     Thomas M. Rasmussen
     Copyright   2000  University of Cambridge
 *)
 
 header {* Bijections between sets *}
 
-theory BijectionRel imports Main begin
+theory BijectionRel
+imports Main
+begin
 
 text {*
   Inductive definitions of bijections between two different sets and
diff -r 8aaa21db41f3 -r e9b4835a54ee src/HOL/Old_Number_Theory/Chinese.thy
--- a/src/HOL/Old_Number_Theory/Chinese.thy	Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Chinese.thy	Fri Aug 06 12:37:00 2010 +0200
@@ -1,4 +1,5 @@
-(*  Author:     Thomas M. Rasmussen
+(*  Title:      HOL/Old_Number_Theory/Chinese.thy
+    Author:     Thomas M. Rasmussen
     Copyright   2000  University of Cambridge
 *)
 
@@ -19,17 +20,15 @@
 
 subsection {* Definitions *}
 
-consts
-  funprod :: "(nat => int) => nat => nat => int"
-  funsum :: "(nat => int) => nat => nat => int"
-
-primrec
+primrec funprod :: "(nat => int) => nat => nat => int"
+where
   "funprod f i 0 = f i"
-  "funprod f i (Suc n) = f (Suc (i + n)) * funprod f i n"
+| "funprod f i (Suc n) = f (Suc (i + n)) * funprod f i n"
 
-primrec
+primrec funsum :: "(nat => int) => nat => nat => int"
+where
   "funsum f i 0 = f i"
-  "funsum f i (Suc n) = f (Suc (i + n)) + funsum f i n"
+| "funsum f i (Suc n) = f (Suc (i + n)) + funsum f i n"
 
 definition
   m_cond :: "nat => (nat => int) => bool" where
diff -r 8aaa21db41f3 -r e9b4835a54ee src/HOL/Old_Number_Theory/Euler.thy
--- a/src/HOL/Old_Number_Theory/Euler.thy	Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Euler.thy	Fri Aug 06 12:37:00 2010 +0200
@@ -1,19 +1,18 @@
-(*  Title:      HOL/Quadratic_Reciprocity/Euler.thy
-    ID:         $Id$
+(*  Title:      HOL/Old_Number_Theory/Euler.thy
     Authors:    Jeremy Avigad, David Gray, and Adam Kramer
 *)
 
 header {* Euler's criterion *}
 
-theory Euler imports Residues EvenOdd begin
+theory Euler
+imports Residues EvenOdd
+begin
 
-definition
-  MultInvPair :: "int => int => int => int set" where
-  "MultInvPair a p j = {StandardRes p j, StandardRes p (a * (MultInv p j))}"
+definition MultInvPair :: "int => int => int => int set"
+  where "MultInvPair a p j = {StandardRes p j, StandardRes p (a * (MultInv p j))}"
 
-definition
-  SetS        :: "int => int => int set set" where
-  "SetS        a p   =  (MultInvPair a p ` SRStar p)"
+definition SetS :: "int => int => int set set"
+  where "SetS a p = MultInvPair a p ` SRStar p"
 
 
 subsection {* Property for MultInvPair *}
diff -r 8aaa21db41f3 -r e9b4835a54ee src/HOL/Old_Number_Theory/EulerFermat.thy
--- a/src/HOL/Old_Number_Theory/EulerFermat.thy	Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/EulerFermat.thy	Fri Aug 06 12:37:00 2010 +0200
@@ -1,4 +1,5 @@
-(*  Author:     Thomas M. Rasmussen
+(*  Title:      HOL/Old_Number_Theory/EulerFermat.thy
+    Author:     Thomas M. Rasmussen
     Copyright   2000  University of Cambridge
 *)
 
@@ -17,49 +18,40 @@
 
 subsection {* Definitions and lemmas *}
 
-inductive_set
-  RsetR :: "int => int set set"
-  for m :: int
-  where
-    empty [simp]: "{} \<in> RsetR m"
-  | 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"
+inductive_set RsetR :: "int => int set set" for m :: int
+where
+  empty [simp]: "{} \<in> RsetR m"
+| 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"
 
-fun
-  BnorRset :: "int \<Rightarrow> int => int set"
-where
+fun BnorRset :: "int \<Rightarrow> int => int set" where
   "BnorRset a m =
    (if 0 < a then
     let na = BnorRset (a - 1) m
     in (if zgcd a m = 1 then insert a na else na)
     else {})"
 
-definition
-  norRRset :: "int => int set" where
-  "norRRset m = BnorRset (m - 1) m"
+definition norRRset :: "int => int set"
+  where "norRRset m = BnorRset (m - 1) m"
 
-definition
-  noXRRset :: "int => int => int set" where
-  "noXRRset m x = (\<lambda>a. a * x) ` norRRset m"
+definition noXRRset :: "int => int => int set"
+  where "noXRRset m x = (\<lambda>a. a * x) ` norRRset m"
 
-definition
-  phi :: "int => nat" where
-  "phi m = card (norRRset m)"
+definition phi :: "int => nat"
+  where "phi m = card (norRRset m)"
 
-definition
-  is_RRset :: "int set => int => bool" where
-  "is_RRset A m = (A \<in> RsetR m \<and> card A = phi m)"
+definition is_RRset :: "int set => int => bool"
+  where "is_RRset A m = (A \<in> RsetR m \<and> card A = phi m)"
 
-definition
-  RRset2norRR :: "int set => int => int => int" where
-  "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)"
+definition RRset2norRR :: "int set => int => int => int"
+  where
+    "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)"
 
-definition
-  zcongm :: "int => int => int => bool" where
-  "zcongm m = (\<lambda>a b. zcong a b m)"
+definition zcongm :: "int => int => int => bool"
+  where "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 8aaa21db41f3 -r e9b4835a54ee src/HOL/Old_Number_Theory/EvenOdd.thy
--- a/src/HOL/Old_Number_Theory/EvenOdd.thy	Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/EvenOdd.thy	Fri Aug 06 12:37:00 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Quadratic_Reciprocity/EvenOdd.thy
+(*  Title:      HOL/Old_Number_Theory/EvenOdd.thy
     Authors:    Jeremy Avigad, David Gray, and Adam Kramer
 *)
 
@@ -8,13 +8,11 @@
 imports Int2
 begin
 
-definition
-  zOdd    :: "int set" where
-  "zOdd = {x. \<exists>k. x = 2 * k + 1}"
+definition zOdd :: "int set"
+  where "zOdd = {x. \<exists>k. x = 2 * k + 1}"
 
-definition
-  zEven   :: "int set" where
-  "zEven = {x. \<exists>k. x = 2 * k}"
+definition zEven :: "int set"
+  where "zEven = {x. \<exists>k. x = 2 * k}"
 
 subsection {* Some useful properties about even and odd *}
 
diff -r 8aaa21db41f3 -r e9b4835a54ee src/HOL/Old_Number_Theory/Factorization.thy
--- a/src/HOL/Old_Number_Theory/Factorization.thy	Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Factorization.thy	Fri Aug 06 12:37:00 2010 +0200
@@ -1,41 +1,39 @@
-(*  Author:     Thomas Marthedal Rasmussen
+(*  Title:      HOL/Old_Number_Theory/Factorization.thy
+    Author:     Thomas Marthedal Rasmussen
     Copyright   2000  University of Cambridge
 *)
 
 header {* Fundamental Theorem of Arithmetic (unique factorization into primes) *}
 
 theory Factorization
-imports Main "~~/src/HOL/Old_Number_Theory/Primes" Permutation
+imports Primes Permutation
 begin
 
 
 subsection {* Definitions *}
 
-definition
-  primel :: "nat list => bool" where
-  "primel xs = (\<forall>p \<in> set xs. prime p)"
+definition primel :: "nat list => bool"
+  where "primel xs = (\<forall>p \<in> set xs. prime p)"
 
-consts
-  nondec :: "nat list => bool "
-  prod :: "nat list => nat"
-  oinsert :: "nat => nat list => nat list"
-  sort :: "nat list => nat list"
-
-primrec
+primrec nondec :: "nat list => bool"
+where
   "nondec [] = True"
-  "nondec (x # xs) = (case xs of [] => True | y # ys => x \<le> y \<and> nondec xs)"
+| "nondec (x # xs) = (case xs of [] => True | y # ys => x \<le> y \<and> nondec xs)"
 
-primrec
+primrec prod :: "nat list => nat"
+where
   "prod [] = Suc 0"
-  "prod (x # xs) = x * prod xs"
+| "prod (x # xs) = x * prod xs"
 
-primrec
+primrec oinsert :: "nat => nat list => nat list"
+where
   "oinsert x [] = [x]"
-  "oinsert x (y # ys) = (if x \<le> y then x # y # ys else y # oinsert x ys)"
+| "oinsert x (y # ys) = (if x \<le> y then x # y # ys else y # oinsert x ys)"
 
-primrec
+primrec sort :: "nat list => nat list"
+where
   "sort [] = []"
-  "sort (x # xs) = oinsert x (sort xs)"
+| "sort (x # xs) = oinsert x (sort xs)"
 
 
 subsection {* Arithmetic *}
diff -r 8aaa21db41f3 -r e9b4835a54ee src/HOL/Old_Number_Theory/Fib.thy
--- a/src/HOL/Old_Number_Theory/Fib.thy	Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Fib.thy	Fri Aug 06 12:37:00 2010 +0200
@@ -1,4 +1,4 @@
-(*  ID:         $Id$
+(*  Title:      HOL/Old_Number_Theory/Fib.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1997  University of Cambridge
 *)
@@ -19,8 +19,8 @@
 
 fun fib :: "nat \<Rightarrow> nat"
 where
-         "fib 0 = 0"
-|        "fib (Suc 0) = 1"
+  "fib 0 = 0"
+| "fib (Suc 0) = 1"
 | fib_2: "fib (Suc (Suc n)) = fib n + fib (Suc n)"
 
 text {*
diff -r 8aaa21db41f3 -r e9b4835a54ee src/HOL/Old_Number_Theory/Finite2.thy
--- a/src/HOL/Old_Number_Theory/Finite2.thy	Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Finite2.thy	Fri Aug 06 12:37:00 2010 +0200
@@ -1,12 +1,11 @@
-(*  Title:      HOL/Quadratic_Reciprocity/Finite2.thy
-    ID:         $Id$
+(*  Title:      HOL/Old_Number_Theory/Finite2.thy
     Authors:    Jeremy Avigad, David Gray, and Adam Kramer
 *)
 
 header {*Finite Sets and Finite Sums*}
 
 theory Finite2
-imports Main IntFact Infinite_Set
+imports IntFact Infinite_Set
 begin
 
 text{*
diff -r 8aaa21db41f3 -r e9b4835a54ee src/HOL/Old_Number_Theory/Gauss.thy
--- a/src/HOL/Old_Number_Theory/Gauss.thy	Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Gauss.thy	Fri Aug 06 12:37:00 2010 +0200
@@ -1,6 +1,5 @@
-(*  Title:      HOL/Quadratic_Reciprocity/Gauss.thy
-    ID:         $Id$
-    Authors:    Jeremy Avigad, David Gray, and Adam Kramer)
+(*  Title:      HOL/Old_Number_Theory/Gauss.thy
+    Authors:    Jeremy Avigad, David Gray, and Adam Kramer
 *)
 
 header {* Gauss' Lemma *}
@@ -19,29 +18,12 @@
   assumes a_nonzero:    "0 < a"
 begin
 
-definition
-  A :: "int set" where
-  "A = {(x::int). 0 < x & x \<le> ((p - 1) div 2)}"
-
-definition
-  B :: "int set" where
-  "B = (%x. x * a) ` A"
-
-definition
-  C :: "int set" where
-  "C = StandardRes p ` B"
-
-definition
-  D :: "int set" where
-  "D = C \<inter> {x. x \<le> ((p - 1) div 2)}"
-
-definition
-  E :: "int set" where
-  "E = C \<inter> {x. ((p - 1) div 2) < x}"
-
-definition
-  F :: "int set" where
-  "F = (%x. (p - x)) ` E"
+definition "A = {(x::int). 0 < x & x \<le> ((p - 1) div 2)}"
+definition "B = (%x. x * a) ` A"
+definition "C = StandardRes p ` B"
+definition "D = C \<inter> {x. x \<le> ((p - 1) div 2)}"
+definition "E = C \<inter> {x. ((p - 1) div 2) < x}"
+definition "F = (%x. (p - x)) ` E"
 
 
 subsection {* Basic properties of p *}
diff -r 8aaa21db41f3 -r e9b4835a54ee src/HOL/Old_Number_Theory/Int2.thy
--- a/src/HOL/Old_Number_Theory/Int2.thy	Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Int2.thy	Fri Aug 06 12:37:00 2010 +0200
@@ -1,5 +1,4 @@
-(*  Title:      HOL/Quadratic_Reciprocity/Gauss.thy
-    ID:         $Id$
+(*  Title:      HOL/Old_Number_Theory/Int2.thy
     Authors:    Jeremy Avigad, David Gray, and Adam Kramer
 *)
 
@@ -9,9 +8,8 @@
 imports Finite2 WilsonRuss
 begin
 
-definition
-  MultInv :: "int => int => int" where
-  "MultInv p x = x ^ nat (p - 2)"
+definition MultInv :: "int => int => int"
+  where "MultInv p x = x ^ nat (p - 2)"
 
 
 subsection {* Useful lemmas about dvd and powers *}
diff -r 8aaa21db41f3 -r e9b4835a54ee src/HOL/Old_Number_Theory/IntFact.thy
--- a/src/HOL/Old_Number_Theory/IntFact.thy	Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/IntFact.thy	Fri Aug 06 12:37:00 2010 +0200
@@ -1,10 +1,13 @@
-(*  Author:     Thomas M. Rasmussen
+(*  Title:      HOL/Old_Number_Theory/IntFact.thy
+    Author:     Thomas M. Rasmussen
     Copyright   2000  University of Cambridge
 *)
 
 header {* Factorial on integers *}
 
-theory IntFact imports IntPrimes begin
+theory IntFact
+imports IntPrimes
+begin
 
 text {*
   Factorial on integers and recursively defined set including all
@@ -14,15 +17,11 @@
   \bigskip
 *}
 
-fun
-  zfact :: "int => int"
-where
-  "zfact n = (if n \<le> 0 then 1 else n * zfact (n - 1))"
+fun zfact :: "int => int"
+  where "zfact n = (if n \<le> 0 then 1 else n * zfact (n - 1))"
 
-fun
-  d22set :: "int => int set"
-where
-  "d22set a = (if 1 < a then insert a (d22set (a - 1)) else {})"
+fun d22set :: "int => int set"
+  where "d22set a = (if 1 < a then insert a (d22set (a - 1)) else {})"
 
 
 text {*
diff -r 8aaa21db41f3 -r e9b4835a54ee src/HOL/Old_Number_Theory/IntPrimes.thy
--- a/src/HOL/Old_Number_Theory/IntPrimes.thy	Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/IntPrimes.thy	Fri Aug 06 12:37:00 2010 +0200
@@ -1,11 +1,12 @@
-(*  Author:     Thomas M. Rasmussen
+(*  Title:      HOL/Old_Number_Theory/IntPrimes.thy
+    Author:     Thomas M. Rasmussen
     Copyright   2000  University of Cambridge
 *)
 
 header {* Divisibility and prime numbers (on integers) *}
 
 theory IntPrimes
-imports Main Primes
+imports Primes
 begin
 
 text {*
@@ -19,8 +20,7 @@
 
 subsection {* Definitions *}
 
-fun
-  xzgcda :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int => (int * int * int)"
+fun xzgcda :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int => (int * int * int)"
 where
   "xzgcda m n r' r s' s t' t =
         (if r \<le> 0 then (r', s', t')
@@ -28,17 +28,15 @@
                       s (s' - (r' div r) * s) 
                       t (t' - (r' div r) * t))"
 
-definition
-  zprime :: "int \<Rightarrow> bool" where
-  "zprime p = (1 < p \<and> (\<forall>m. 0 <= m & m dvd p --> m = 1 \<or> m = p))"
+definition zprime :: "int \<Rightarrow> bool"
+  where "zprime p = (1 < p \<and> (\<forall>m. 0 <= m & m dvd p --> m = 1 \<or> m = p))"
 
-definition
-  xzgcd :: "int => int => int * int * int" where
-  "xzgcd m n = xzgcda m n m n 1 0 0 1"
+definition xzgcd :: "int => int => int * int * int"
+  where "xzgcd m n = xzgcda m n m n 1 0 0 1"
 
-definition
-  zcong :: "int => int => int => bool"  ("(1[_ = _] '(mod _'))") where
-  "[a = b] (mod m) = (m dvd (a - b))"
+definition zcong :: "int => int => int => bool"  ("(1[_ = _] '(mod _'))")
+  where "[a = b] (mod m) = (m dvd (a - b))"
+
 
 subsection {* Euclid's Algorithm and GCD *}
 
diff -r 8aaa21db41f3 -r e9b4835a54ee src/HOL/Old_Number_Theory/Legacy_GCD.thy
--- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Fri Aug 06 12:37:00 2010 +0200
@@ -38,17 +38,17 @@
 
 subsection {* GCD on nat by Euclid's algorithm *}
 
-fun
-  gcd  :: "nat => nat => nat"
-where
-  "gcd m n = (if n = 0 then m else gcd n (m mod n))"
+fun gcd :: "nat => nat => nat"
+  where "gcd m n = (if n = 0 then m else gcd n (m mod n))"
+
 lemma gcd_induct [case_names "0" rec]:
   fixes m n :: nat
   assumes "\<And>m. P m 0"
     and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
   shows "P m n"
 proof (induct m n rule: gcd.induct)
-  case (1 m n) with assms show ?case by (cases "n = 0") simp_all
+  case (1 m n)
+  with assms show ?case by (cases "n = 0") simp_all
 qed
 
 lemma gcd_0 [simp, algebra]: "gcd m 0 = m"
@@ -751,22 +751,22 @@
 
 lemma lcm_pos: 
   assumes mpos: "m > 0"
-  and npos: "n>0"
+    and npos: "n>0"
   shows "lcm m n > 0"
-proof(rule ccontr, simp add: lcm_def gcd_zero)
-assume h:"m*n div gcd m n = 0"
-from mpos npos have "gcd m n \<noteq> 0" using gcd_zero by simp
-hence gcdp: "gcd m n > 0" by simp
-with h
-have "m*n < gcd m n"
-  by (cases "m * n < gcd m n") (auto simp add: div_if[OF gcdp, where m="m*n"])
-moreover 
-have "gcd m n dvd m" by simp
- with mpos dvd_imp_le have t1:"gcd m n \<le> m" by simp
- with npos have t1:"gcd m n *n \<le> m*n" by simp
- have "gcd m n \<le> gcd m n*n" using npos by simp
- with t1 have "gcd m n \<le> m*n" by arith
-ultimately show "False" by simp
+proof (rule ccontr, simp add: lcm_def gcd_zero)
+  assume h:"m*n div gcd m n = 0"
+  from mpos npos have "gcd m n \<noteq> 0" using gcd_zero by simp
+  hence gcdp: "gcd m n > 0" by simp
+  with h
+  have "m*n < gcd m n"
+    by (cases "m * n < gcd m n") (auto simp add: div_if[OF gcdp, where m="m*n"])
+  moreover 
+  have "gcd m n dvd m" by simp
+  with mpos dvd_imp_le have t1:"gcd m n \<le> m" by simp
+  with npos have t1:"gcd m n *n \<le> m*n" by simp
+  have "gcd m n \<le> gcd m n*n" using npos by simp
+  with t1 have "gcd m n \<le> m*n" by arith
+  ultimately show "False" by simp
 qed
 
 lemma zlcm_pos: 
diff -r 8aaa21db41f3 -r e9b4835a54ee src/HOL/Old_Number_Theory/Pocklington.thy
--- a/src/HOL/Old_Number_Theory/Pocklington.thy	Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Pocklington.thy	Fri Aug 06 12:37:00 2010 +0200
@@ -1,11 +1,11 @@
-(*  Title:      HOL/Library/Pocklington.thy
+(*  Title:      HOL/Old_Number_Theory/Pocklington.thy
     Author:     Amine Chaieb
 *)
 
 header {* Pocklington's Theorem for Primes *}
 
 theory Pocklington
-imports Main Primes
+imports Primes
 begin
 
 definition modeq:: "nat => nat => nat => bool"    ("(1[_ = _] '(mod _'))")
diff -r 8aaa21db41f3 -r e9b4835a54ee src/HOL/Old_Number_Theory/Primes.thy
--- a/src/HOL/Old_Number_Theory/Primes.thy	Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Primes.thy	Fri Aug 06 12:37:00 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Library/Primes.thy
+(*  Title:      HOL/Old_Number_Theory/Primes.thy
     Author:     Amine Chaieb, Christophe Tabacznyj and Lawrence C Paulson
     Copyright   1996  University of Cambridge
 *)
@@ -9,13 +9,11 @@
 imports Complex_Main Legacy_GCD
 begin
 
-definition
-  coprime :: "nat => nat => bool" where
-  "coprime m n \<longleftrightarrow> gcd m n = 1"
+definition coprime :: "nat => nat => bool"
+  where "coprime m n \<longleftrightarrow> gcd m n = 1"
 
-definition
-  prime :: "nat \<Rightarrow> bool" where
-  "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
+definition prime :: "nat \<Rightarrow> bool"
+  where "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
 
 
 lemma two_is_prime: "prime 2"
diff -r 8aaa21db41f3 -r e9b4835a54ee src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
--- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Fri Aug 06 12:37:00 2010 +0200
@@ -1,4 +1,5 @@
-(*  Authors:    Jeremy Avigad, David Gray, and Adam Kramer
+(*  Title:      HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
+    Authors:    Jeremy Avigad, David Gray, and Adam Kramer
 *)
 
 header {* The law of Quadratic reciprocity *}
@@ -165,33 +166,26 @@
   assumes p_neq_q:      "p \<noteq> q"
 begin
 
-definition
-  P_set :: "int set" where
-  "P_set = {x. 0 < x & x \<le> ((p - 1) div 2) }"
+definition P_set :: "int set"
+  where "P_set = {x. 0 < x & x \<le> ((p - 1) div 2) }"
 
-definition
-  Q_set :: "int set" where
-  "Q_set = {x. 0 < x & x \<le> ((q - 1) div 2) }"
+definition Q_set :: "int set"
+  where "Q_set = {x. 0 < x & x \<le> ((q - 1) div 2) }"
   
-definition
-  S :: "(int * int) set" where
-  "S = P_set <*> Q_set"
+definition S :: "(int * int) set"
+  where "S = P_set <*> Q_set"
 
-definition
-  S1 :: "(int * int) set" where
-  "S1 = { (x, y). (x, y):S & ((p * y) < (q * x)) }"
+definition S1 :: "(int * int) set"
+  where "S1 = { (x, y). (x, y):S & ((p * y) < (q * x)) }"
 
-definition
-  S2 :: "(int * int) set" where
-  "S2 = { (x, y). (x, y):S & ((q * x) < (p * y)) }"
+definition S2 :: "(int * int) set"
+  where "S2 = { (x, y). (x, y):S & ((q * x) < (p * y)) }"
 
-definition
-  f1 :: "int => (int * int) set" where
-  "f1 j = { (j1, y). (j1, y):S & j1 = j & (y \<le> (q * j) div p) }"
+definition f1 :: "int => (int * int) set"
+  where "f1 j = { (j1, y). (j1, y):S & j1 = j & (y \<le> (q * j) div p) }"
 
-definition
-  f2 :: "int => (int * int) set" where
-  "f2 j = { (x, j1). (x, j1):S & j1 = j & (x \<le> (p * j) div q) }"
+definition f2 :: "int => (int * int) set"
+  where "f2 j = { (x, j1). (x, j1):S & j1 = j & (x \<le> (p * j) div q) }"
 
 lemma p_fact: "0 < (p - 1) div 2"
 proof -
diff -r 8aaa21db41f3 -r e9b4835a54ee src/HOL/Old_Number_Theory/Residues.thy
--- a/src/HOL/Old_Number_Theory/Residues.thy	Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Residues.thy	Fri Aug 06 12:37:00 2010 +0200
@@ -1,41 +1,36 @@
-(*  Title:      HOL/Quadratic_Reciprocity/Residues.thy
-    ID:         $Id$
+(*  Title:      HOL/Old_Number_Theory/Residues.thy
     Authors:    Jeremy Avigad, David Gray, and Adam Kramer
 *)
 
 header {* Residue Sets *}
 
-theory Residues imports Int2 begin
+theory Residues
+imports Int2
+begin
 
 text {*
   \medskip Define the residue of a set, the standard residue,
   quadratic residues, and prove some basic properties. *}
 
-definition
-  ResSet      :: "int => int set => bool" where
-  "ResSet m X = (\<forall>y1 y2. (y1 \<in> X & y2 \<in> X & [y1 = y2] (mod m) --> y1 = y2))"
+definition ResSet :: "int => int set => bool"
+  where "ResSet m X = (\<forall>y1 y2. (y1 \<in> X & y2 \<in> X & [y1 = y2] (mod m) --> y1 = y2))"
 
-definition
-  StandardRes :: "int => int => int" where
-  "StandardRes m x = x mod m"
+definition StandardRes :: "int => int => int"
+  where "StandardRes m x = x mod m"
 
-definition
-  QuadRes     :: "int => int => bool" where
-  "QuadRes m x = (\<exists>y. ([(y ^ 2) = x] (mod m)))"
+definition QuadRes :: "int => int => bool"
+  where "QuadRes m x = (\<exists>y. ([(y ^ 2) = x] (mod m)))"
 
-definition
-  Legendre    :: "int => int => int" where
+definition Legendre :: "int => int => int" where
   "Legendre a p = (if ([a = 0] (mod p)) then 0
                      else if (QuadRes p a) then 1
                      else -1)"
 
-definition
-  SR          :: "int => int set" where
-  "SR p = {x. (0 \<le> x) & (x < p)}"
+definition SR :: "int => int set"
+  where "SR p = {x. (0 \<le> x) & (x < p)}"
 
-definition
-  SRStar      :: "int => int set" where
-  "SRStar p = {x. (0 < x) & (x < p)}"
+definition SRStar :: "int => int set"
+  where "SRStar p = {x. (0 < x) & (x < p)}"
 
 
 subsection {* Some useful properties of StandardRes *}
diff -r 8aaa21db41f3 -r e9b4835a54ee src/HOL/Old_Number_Theory/WilsonBij.thy
--- a/src/HOL/Old_Number_Theory/WilsonBij.thy	Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/WilsonBij.thy	Fri Aug 06 12:37:00 2010 +0200
@@ -1,10 +1,13 @@
-(*  Author:     Thomas M. Rasmussen
+(*  Title:      HOL/Old_Number_Theory/WilsonBij.thy
+    Author:     Thomas M. Rasmussen
     Copyright   2000  University of Cambridge
 *)
 
 header {* Wilson's Theorem using a more abstract approach *}
 
-theory WilsonBij imports BijectionRel IntFact begin
+theory WilsonBij
+imports BijectionRel IntFact
+begin
 
 text {*
   Wilson's Theorem using a more ``abstract'' approach based on
@@ -15,12 +18,10 @@
 
 subsection {* Definitions and lemmas *}
 
-definition
-  reciR :: "int => int => int => bool" where
-  "reciR p = (\<lambda>a b. zcong (a * b) 1 p \<and> 1 < a \<and> a < p - 1 \<and> 1 < b \<and> b < p - 1)"
+definition reciR :: "int => int => int => bool"
+  where "reciR p = (\<lambda>a b. zcong (a * b) 1 p \<and> 1 < a \<and> a < p - 1 \<and> 1 < b \<and> b < p - 1)"
 
-definition
-  inv :: "int => int => int" where
+definition inv :: "int => int => int" where
   "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)
diff -r 8aaa21db41f3 -r e9b4835a54ee src/HOL/Old_Number_Theory/WilsonRuss.thy
--- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Fri Aug 06 12:37:00 2010 +0200
@@ -1,10 +1,13 @@
-(*  Author:     Thomas M. Rasmussen
+(*  Title:      HOL/Old_Number_Theory/WilsonRuss.thy
+    Author:     Thomas M. Rasmussen
     Copyright   2000  University of Cambridge
 *)
 
 header {* Wilson's Theorem according to Russinoff *}
 
-theory WilsonRuss imports EulerFermat begin
+theory WilsonRuss
+imports EulerFermat
+begin
 
 text {*
   Wilson's Theorem following quite closely Russinoff's approach
@@ -13,13 +16,10 @@
 
 subsection {* Definitions and lemmas *}
 
-definition
-  inv :: "int => int => int" where
-  "inv p a = (a^(nat (p - 2))) mod p"
+definition inv :: "int => int => int"
+  where "inv p a = (a^(nat (p - 2))) mod p"
 
-fun
-  wset :: "int \<Rightarrow> int => int set"
-where
+fun wset :: "int \<Rightarrow> int => int set" where
   "wset a p =
     (if 1 < a then
       let ws = wset (a - 1) p
@@ -29,7 +29,7 @@
 text {* \medskip @{term [source] inv} *}
 
 lemma inv_is_inv_aux: "1 < m ==> Suc (nat (m - 2)) = nat (m - 1)"
-by (subst int_int_eq [symmetric], auto)
+  by (subst int_int_eq [symmetric]) auto
 
 lemma inv_is_inv:
     "zprime p \<Longrightarrow> 0 < a \<Longrightarrow> a < p ==> [a * inv p a = 1] (mod p)"