# HG changeset patch
# User wenzelm
# Date 1082081230 -7200
# Node ID dbb95b8252449f3a0cddcbff06f9f7926e19e9f4
# Parent  37a92211a5d363610fea965e3b928c8f183aafba
tuned document;

diff -r 37a92211a5d3 -r dbb95b825244 src/HOL/Algebra/CRing.thy
--- a/src/HOL/Algebra/CRing.thy	Fri Apr 16 04:06:52 2004 +0200
+++ b/src/HOL/Algebra/CRing.thy	Fri Apr 16 04:07:10 2004 +0200
@@ -5,11 +5,11 @@
   Copyright: Clemens Ballarin
 *)
 
+header {* Abelian Groups *}
+
 theory CRing = FiniteProduct
 files ("ringsimp.ML"):
 
-section {* Abelian Groups *}
-
 record 'a ring = "'a monoid" +
   zero :: 'a ("\<zero>\<index>")
   add :: "['a, 'a] => 'a" (infixl "\<oplus>\<index>" 65)
diff -r 37a92211a5d3 -r dbb95b825244 src/HOL/Algebra/Lattice.thy
--- a/src/HOL/Algebra/Lattice.thy	Fri Apr 16 04:06:52 2004 +0200
+++ b/src/HOL/Algebra/Lattice.thy	Fri Apr 16 04:07:10 2004 +0200
@@ -5,9 +5,9 @@
   Copyright: Clemens Ballarin
 *)
 
-theory Lattice = Group:
+header {* Order and Lattices *}
 
-section {* Order and Lattices *}
+theory Lattice = Group:
 
 subsection {* Partial Orders *}
 
diff -r 37a92211a5d3 -r dbb95b825244 src/HOL/Algebra/Module.thy
--- a/src/HOL/Algebra/Module.thy	Fri Apr 16 04:06:52 2004 +0200
+++ b/src/HOL/Algebra/Module.thy	Fri Apr 16 04:07:10 2004 +0200
@@ -4,9 +4,9 @@
     Copyright:  Clemens Ballarin
 *)
 
-theory Module = CRing:
+header {* Modules over an Abelian Group *}
 
-section {* Modules over an Abelian Group *}
+theory Module = CRing:
 
 record ('a, 'b) module = "'b ring" +
   smult :: "['a, 'b] => 'b" (infixl "\<odot>\<index>" 70)
diff -r 37a92211a5d3 -r dbb95b825244 src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Fri Apr 16 04:06:52 2004 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Fri Apr 16 04:07:10 2004 +0200
@@ -5,9 +5,9 @@
   Copyright: Clemens Ballarin
 *)
 
-theory UnivPoly = Module:
+header {* Univariate Polynomials *}
 
-section {* Univariate Polynomials *}
+theory UnivPoly = Module:
 
 text {*
   Polynomials are formalised as modules with additional operations for 
diff -r 37a92211a5d3 -r dbb95b825244 src/HOL/Integ/NatSimprocs.thy
--- a/src/HOL/Integ/NatSimprocs.thy	Fri Apr 16 04:06:52 2004 +0200
+++ b/src/HOL/Integ/NatSimprocs.thy	Fri Apr 16 04:07:10 2004 +0200
@@ -17,8 +17,9 @@
 lemma Suc_diff_eq_diff_pred: "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)"
 by (simp add: numeral_0_eq_0 numeral_1_eq_1 split add: nat_diff_split)
 
-(*Now just instantiating n to (number_of v) does the right simplification,
-  but with some redundant inequality tests.*)
+text {*Now just instantiating @{text n} to @{text "number_of v"} does
+  the right simplification, but with some redundant inequality
+  tests.*}
 lemma neg_number_of_bin_pred_iff_0:
      "neg (number_of (bin_pred v)::int) = (number_of v = (0::nat))"
 apply (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < Suc 0) ")
@@ -171,8 +172,9 @@
 declare zero_le_divide_iff [of "number_of w", standard, simp]
 declare divide_le_0_iff [of "number_of w", standard, simp]
 
-(*Replaces "inverse #nn" by 1/#nn.  It looks strange, but then other simprocs
-simplify the quotient.*)
+text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}.  It looks
+  strange, but then other simprocs simplify the quotient.*}
+
 declare inverse_eq_divide [of "number_of w", standard, simp]
 
 text{*These laws simplify inequalities, moving unary minus from a term
@@ -194,16 +196,14 @@
 declare minus_le_iff [of _ 1, simplified, simp]
 declare minus_equation_iff [of _ 1, simplified, simp]
 
-
-(*Cancellation of constant factors in comparisons (< and \<le>) *)
+text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
 
 declare mult_less_cancel_left [of "number_of v", standard, simp]
 declare mult_less_cancel_right [of _ "number_of v", standard, simp]
 declare mult_le_cancel_left [of "number_of v", standard, simp]
 declare mult_le_cancel_right [of _ "number_of v", standard, simp]
 
-
-(*Multiplying out constant divisors in comparisons (< \<le> and =) *)
+text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *}
 
 declare le_divide_eq [of _ _ "number_of w", standard, simp]
 declare divide_le_eq [of _ "number_of w", standard, simp]
diff -r 37a92211a5d3 -r dbb95b825244 src/HOL/Integ/Presburger.thy
--- a/src/HOL/Integ/Presburger.thy	Fri Apr 16 04:06:52 2004 +0200
+++ b/src/HOL/Integ/Presburger.thy	Fri Apr 16 04:07:10 2004 +0200
@@ -7,6 +7,8 @@
 generation for Cooper Algorithm  
 *)
 
+header {* Presburger Arithmetic: Cooper Algorithm *}
+
 theory Presburger = NatSimprocs + SetInterval
 files
   ("cooper_dec.ML")
@@ -14,7 +16,7 @@
   ("qelim.ML")
   ("presburger.ML"):
 
-(* Theorem for unitifying the coeffitients of x in an existential formula*)
+text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*}
 
 theorem unity_coeff_ex: "(\<exists>x::int. P (l * x)) = (\<exists>x. l dvd (1*x+0) \<and> P x)"
   apply (rule iffI)
@@ -54,7 +56,7 @@
 
 
 
-(*Theorems for the combination of proofs of the equality of P and P_m for integers x less than some integer z.*)
+text {*Theorems for the combination of proofs of the equality of @{text P} and @{text P_m} for integers @{text x} less than some integer @{text z}.*}
 
 theorem eq_minf_conjI: "\<exists>z1::int. \<forall>x. x < z1 \<longrightarrow> (A1 x = A2 x) \<Longrightarrow>
   \<exists>z2::int. \<forall>x. x < z2 \<longrightarrow> (B1 x = B2 x) \<Longrightarrow>
@@ -75,7 +77,7 @@
   done
 
 
-(*Theorems for the combination of proofs of the equality of P and P_m for integers x greather than some integer z.*)
+text {*Theorems for the combination of proofs of the equality of @{text P} and @{text P_m} for integers @{text x} greather than some integer @{text z}.*}
 
 theorem eq_pinf_conjI: "\<exists>z1::int. \<forall>x. z1 < x \<longrightarrow> (A1 x = A2 x) \<Longrightarrow>
   \<exists>z2::int. \<forall>x. z2 < x \<longrightarrow> (B1 x = B2 x) \<Longrightarrow>
@@ -93,75 +95,76 @@
   apply (rule_tac x = "max z1 z2" in exI)
   apply simp
   done
-(*=============================================================================*)
-(*Theorems for the combination of proofs of the modulo D property for P
-pluusinfinity*)
-(* FIXME : This is THE SAME theorem as for the minusinf version, but with +k.. instead of -k.. In the future replace these both with only one*)
+
+text {*
+  \medskip Theorems for the combination of proofs of the modulo @{text
+  D} property for @{text "P plusinfinity"}
+
+  FIXME: This is THE SAME theorem as for the @{text minusinf} version,
+  but with @{text "+k.."} instead of @{text "-k.."} In the future
+  replace these both with only one. *}
 
 theorem modd_pinf_conjI: "\<forall>(x::int) k. A x = A (x+k*d) \<Longrightarrow>
   \<forall>(x::int) k. B x = B (x+k*d) \<Longrightarrow>
   \<forall>(x::int) (k::int). (A x \<and> B x) = (A (x+k*d) \<and> B (x+k*d))"
   by simp
 
-
 theorem modd_pinf_disjI: "\<forall>(x::int) k. A x = A (x+k*d) \<Longrightarrow>
   \<forall>(x::int) k. B x = B (x+k*d) \<Longrightarrow>
   \<forall>(x::int) (k::int). (A x \<or> B x) = (A (x+k*d) \<or> B (x+k*d))"
   by simp
 
-(*=============================================================================*)
-(*This is one of the cases where the simplifed formula is prooved to habe some property
-(in relation to P_m) but we need to proove the property for the original formula (P_m)*)
-(*FIXME : This is exaclty the same thm as for minusinf.*)
+text {*
+  This is one of the cases where the simplifed formula is prooved to
+  habe some property (in relation to @{text P_m}) but we need to prove
+  the property for the original formula (@{text P_m})
+
+  FIXME: This is exaclty the same thm as for @{text minusinf}. *}
+
 lemma pinf_simp_eq: "ALL x. P(x) = Q(x) ==> (EX (x::int). P(x)) --> (EX (x::int). F(x))  ==> (EX (x::int). Q(x)) --> (EX (x::int). F(x)) "
-by blast
+  by blast
 
 
-
-(*=============================================================================*)
-(*Theorems for the combination of proofs of the modulo D property for P
-minusinfinity*)
+text {*
+  \medskip Theorems for the combination of proofs of the modulo @{text D}
+  property for @{text "P minusinfinity"} *}
 
 theorem modd_minf_conjI: "\<forall>(x::int) k. A x = A (x-k*d) \<Longrightarrow>
   \<forall>(x::int) k. B x = B (x-k*d) \<Longrightarrow>
   \<forall>(x::int) (k::int). (A x \<and> B x) = (A (x-k*d) \<and> B (x-k*d))"
   by simp
 
-
 theorem modd_minf_disjI: "\<forall>(x::int) k. A x = A (x-k*d) \<Longrightarrow>
   \<forall>(x::int) k. B x = B (x-k*d) \<Longrightarrow>
   \<forall>(x::int) (k::int). (A x \<or> B x) = (A (x-k*d) \<or> B (x-k*d))"
   by simp
 
-(*=============================================================================*)
-(*This is one of the cases where the simplifed formula is prooved to habe some property
-(in relation to P_m) but we need to proove the property for the original formula (P_m)*)
+text {*
+  This is one of the cases where the simplifed formula is prooved to
+  have some property (in relation to @{text P_m}) but we need to
+  prove the property for the original formula (@{text P_m}). *}
 
 lemma minf_simp_eq: "ALL x. P(x) = Q(x) ==> (EX (x::int). P(x)) --> (EX (x::int). F(x))  ==> (EX (x::int). Q(x)) --> (EX (x::int). F(x)) "
-by blast
+  by blast
 
-(*=============================================================================*)
-
-(*theorem needed for prooving at runtime divide properties using the arithmetic tatic
-(who knows only about modulo = 0)*)
+text {*
+  Theorem needed for proving at runtime divide properties using the
+  arithmetic tactic (which knows only about modulo = 0). *}
 
 lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
-by(simp add:dvd_def zmod_eq_0_iff)
-
-(*=============================================================================*)
+  by(simp add:dvd_def zmod_eq_0_iff)
 
-
-
-(*Theorems used for the combination of proof for the backwards direction of cooper's
-theorem. they rely exclusively on Predicate calculus.*)
+text {*
+  \medskip Theorems used for the combination of proof for the
+  backwards direction of Cooper's Theorem. They rely exclusively on
+  Predicate calculus.*}
 
 lemma not_ast_p_disjI: "(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> P1(x) --> P1(x + d))
 ==>
 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> P2(x) --> P2(x + d))
 ==>
 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) -->(P1(x) \<or> P2(x)) --> (P1(x + d) \<or> P2(x + d))) "
-by blast
-
+  by blast
 
 
 lemma not_ast_p_conjI: "(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a- j)) --> P1(x) --> P1(x + d))
@@ -170,18 +173,18 @@
 ==>
 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) -->(P1(x) \<and> P2(x)) --> (P1(x + d)
 \<and> P2(x + d))) "
-by blast
+  by blast
 
 lemma not_ast_p_Q_elim: "
 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) -->P(x) --> P(x + d))
 ==> ( P = Q )
 ==> (ALL x. ~(EX (j::int) : {1..d}. EX (a::int) : A. P(a - j)) -->P(x) --> P(x + d))"
-by blast
-(*=============================================================================*)
+  by blast
 
-
-(*Theorems used for the combination of proof for the backwards direction of cooper's
-theorem. they rely exclusively on Predicate calculus.*)
+text {*
+  \medskip Theorems used for the combination of proof for the
+  backwards direction of Cooper's Theorem. They rely exclusively on
+  Predicate calculus.*}
 
 lemma not_bst_p_disjI: "(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> P1(x) --> P1(x - d))
 ==>
@@ -189,9 +192,7 @@
 ==>
 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) -->(P1(x) \<or> P2(x)) --> (P1(x - d)
 \<or> P2(x-d))) "
-by blast
-
-
+  by blast
 
 lemma not_bst_p_conjI: "(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> P1(x) --> P1(x - d))
 ==>
@@ -199,68 +200,67 @@
 ==>
 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) -->(P1(x) \<and> P2(x)) --> (P1(x - d)
 \<and> P2(x-d))) "
-by blast
+  by blast
 
 lemma not_bst_p_Q_elim: "
 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) -->P(x) --> P(x - d)) 
 ==> ( P = Q )
 ==> (ALL x. ~(EX (j::int) : {1..d}. EX (b::int) : B. P(b+j)) -->P(x) --> P(x - d))"
-by blast
-(*=============================================================================*)
+  by blast
 
-(*This is the first direction of cooper's theorem*)
+text {* \medskip This is the first direction of Cooper's Theorem. *}
 lemma cooper_thm: "(R --> (EX x::int. P x))  ==> (Q -->(EX x::int.  P x )) ==> ((R|Q) --> (EX x::int. P x )) "
-by blast
+  by blast
 
-(*=============================================================================*)
-(*The full cooper's theoorem in its equivalence Form- Given the premisses it is trivial
-too, it relies exclusively on prediacte calculus.*)
+text {*
+  \medskip The full Cooper's Theorem in its equivalence Form. Given
+  the premises it is trivial too, it relies exclusively on prediacte calculus.*}
 lemma cooper_eq_thm: "(R --> (EX x::int. P x))  ==> (Q -->(EX x::int.  P x )) ==> ((~Q)
 --> (EX x::int. P x ) --> R) ==> (EX x::int. P x) = R|Q "
-by blast
+  by blast
 
-(*=============================================================================*)
-(*Some of the atomic theorems generated each time the atom does not depend on x, they
-are trivial.*)
+text {*
+  \medskip Some of the atomic theorems generated each time the atom
+  does not depend on @{text x}, they are trivial.*}
 
 lemma  fm_eq_minf: "EX z::int. ALL x. x < z --> (P = P) "
-by blast
+  by blast
 
 lemma  fm_modd_minf: "ALL (x::int). ALL (k::int). (P = P)"
-by blast
+  by blast
 
 lemma not_bst_p_fm: "ALL (x::int). Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> fm --> fm"
-by blast
-
-
+  by blast
 
 lemma  fm_eq_pinf: "EX z::int. ALL x. z < x --> (P = P) "
-by blast
+  by blast
 
-(* The next 2 thms are the same as the minusinf version*)
+text {* The next two thms are the same as the @{text minusinf} version. *}
+
 lemma  fm_modd_pinf: "ALL (x::int). ALL (k::int). (P = P)"
-by blast
+  by blast
 
 lemma not_ast_p_fm: "ALL (x::int). Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> fm --> fm"
-by blast
+  by blast
 
+text {* Theorems to be deleted from simpset when proving simplified formulaes. *}
 
-(* Theorems to be deleted from simpset when proving simplified formulaes*)
 lemma P_eqtrue: "(P=True) = P"
   by rules
 
 lemma P_eqfalse: "(P=False) = (~P)"
   by rules
 
-(*=============================================================================*)
+text {*
+  \medskip Theorems for the generation of the bachwards direction of
+  Cooper's Theorem.
 
-(*Theorems for the generation of the bachwards direction of cooper's theorem*)
-(*These are the 6 interesting atomic cases which have to be proved relying on the
-properties of B-set ant the arithmetic and contradiction proofs*)
+  These are the 6 interesting atomic cases which have to be proved relying on the
+  properties of B-set and the arithmetic and contradiction proofs. *}
 
 lemma not_bst_p_lt: "0 < (d::int) ==>
  ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> ( 0 < -x + a) --> (0 < -(x - d) + a )"
-by arith
+  by arith
 
 lemma not_bst_p_gt: "\<lbrakk> (g::int) \<in> B; g = -a \<rbrakk> \<Longrightarrow>
  ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> (0 < (x) + a) --> ( 0 < (x - d) + a)"
@@ -315,16 +315,17 @@
 apply(simp add:int_distrib)
 done
 
-
+text {*
+  \medskip Theorems for the generation of the bachwards direction of
+  Cooper's Theorem.
 
-(*Theorems for the generation of the bachwards direction of cooper's theorem*)
-(*These are the 6 interesting atomic cases which have to be proved relying on the
-properties of A-set ant the arithmetic and contradiction proofs*)
+  These are the 6 interesting atomic cases which have to be proved
+  relying on the properties of A-set ant the arithmetic and
+  contradiction proofs. *}
 
 lemma not_ast_p_gt: "0 < (d::int) ==>
  ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> ( 0 < x + t) --> (0 < (x + d) + t )"
-by arith
-
+  by arith
 
 lemma not_ast_p_lt: "\<lbrakk>0 < d ;(t::int) \<in> A \<rbrakk> \<Longrightarrow>
  ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> (0 < -x + t) --> ( 0 < -(x + d) + t)"
@@ -377,12 +378,11 @@
   apply(simp add:int_distrib)
   done
 
-
+text {*
+  \medskip These are the atomic cases for the proof generation for the
+  modulo @{text D} property for @{text "P plusinfinity"}
 
-(*=============================================================================*)
-(*These are the atomic cases for the proof generation for the modulo D property for P
-plusinfinity*)
-(*They are fully based on arithmetics*)
+  They are fully based on arithmetics. *}
 
 lemma  dvd_modd_pinf: "((d::int) dvd d1) ==>
  (ALL (x::int). ALL (k::int). (((d::int) dvd (x + t)) = (d dvd (x+k*d1 + t))))"
@@ -412,10 +412,12 @@
   apply(simp add:int_distrib mult_ac)
   done
 
-(*=============================================================================*)
-(*These are the atomic cases for the proof generation for the equivalence of P and P
-plusinfinity for integers x greather than some integer z.*)
-(*They are fully based on arithmetics*)
+text {*
+  \medskip These are the atomic cases for the proof generation for the
+  equivalence of @{text P} and @{text "P plusinfinity"} for integers
+  @{text x} greater than some integer @{text z}.
+
+  They are fully based on arithmetics. *}
 
 lemma  eq_eq_pinf: "EX z::int. ALL x. z < x --> (( 0 = x +t ) = False )"
   apply(rule_tac x = "-t" in exI)
@@ -438,18 +440,16 @@
   done
 
 lemma  dvd_eq_pinf: "EX z::int. ALL x.  z < x --> ((d dvd (x + t)) = (d dvd (x + t))) "
-by simp
+  by simp
 
 lemma  not_dvd_eq_pinf: "EX z::int. ALL x. z < x  --> ((~(d dvd (x + t))) = (~(d dvd (x + t)))) "
-by simp
-
-
-
+  by simp
 
-(*=============================================================================*)
-(*These are the atomic cases for the proof generation for the modulo D property for P
-minusinfinity*)
-(*They are fully based on arithmetics*)
+text {*
+  \medskip These are the atomic cases for the proof generation for the
+  modulo @{text D} property for @{text "P minusinfinity"}.
+
+  They are fully based on arithmetics. *}
 
 lemma  dvd_modd_minf: "((d::int) dvd d1) ==>
  (ALL (x::int). ALL (k::int). (((d::int) dvd (x + t)) = (d dvd (x-k*d1 + t))))"
@@ -480,11 +480,12 @@
 apply(simp add:int_distrib mult_ac)
 done
 
+text {*
+  \medskip These are the atomic cases for the proof generation for the
+  equivalence of @{text P} and @{text "P minusinfinity"} for integers
+  @{text x} less than some integer @{text z}.
 
-(*=============================================================================*)
-(*These are the atomic cases for the proof generation for the equivalence of P and P
-minusinfinity for integers x less than some integer z.*)
-(*They are fully based on arithmetics*)
+  They are fully based on arithmetics. *}
 
 lemma  eq_eq_minf: "EX z::int. ALL x. x < z --> (( 0 = x +t ) = False )"
 apply(rule_tac x = "-t" in exI)
@@ -508,17 +509,18 @@
 done
 
 lemma  dvd_eq_minf: "EX z::int. ALL x. x < z --> ((d dvd (x + t)) = (d dvd (x + t))) "
-by simp
+  by simp
 
 lemma  not_dvd_eq_minf: "EX z::int. ALL x. x < z --> ((~(d dvd (x + t))) = (~(d dvd (x + t)))) "
-by simp
-
+  by simp
 
-(*=============================================================================*)
-(*This Theorem combines whithnesses about P minusinfinity to schow one component of the
-equivalence proof for cooper's theorem*)
+text {*
+  \medskip This Theorem combines whithnesses about @{text "P
+  minusinfinity"} to show one component of the equivalence proof for
+  Cooper's Theorem.
 
-(* FIXME: remove once they are part of the distribution *)
+  FIXME: remove once they are part of the distribution. *}
+
 theorem int_ge_induct[consumes 1,case_names base step]:
   assumes ge: "k \<le> (i::int)" and
         base: "P(k)" and
@@ -590,9 +592,10 @@
   qed
 qed
 
-(*=============================================================================*)
-(*This Theorem combines whithnesses about P minusinfinity to schow one component of the
-equivalence proof for cooper's theorem*)
+text {*
+  \medskip This Theorem combines whithnesses about @{text "P
+  minusinfinity"} to show one component of the equivalence proof for
+  Cooper's Theorem. *}
 
 lemma plusinfinity:
   assumes "0 < d" and
@@ -613,10 +616,8 @@
   qed
 qed
  
-
-
-(*=============================================================================*)
-(*Theorem for periodic function on discrete sets*)
+text {*
+  \medskip Theorem for periodic function on discrete sets. *}
 
 lemma minf_vee:
   assumes dpos: "(0::int) < d" and modd: "ALL x k. P x = P(x - k*d)"
@@ -651,8 +652,9 @@
   assume ?RHS thus ?LHS by blast
 qed
 
-(*=============================================================================*)
-(*Theorem for periodic function on discrete sets*)
+text {*
+  \medskip Theorem for periodic function on discrete sets. *}
+
 lemma pinf_vee:
   assumes dpos: "0 < (d::int)" and modd: "ALL (x::int) (k::int). P x = P (x+k*d)"
   shows "(EX x::int. P x) = (EX (j::int) : {1..d} . P j)"
@@ -750,7 +752,7 @@
 apply(blast dest:decr_mult_lemma)
 done
 
-(* Cooper Thm `, plus infinity version*)
+text {* Cooper Theorem, plus infinity version. *}
 lemma cppi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. z < x --> (P x = P1 x))
 ==> ALL x.~(EX (j::int) : {1..D}. EX (a::int) : A. P(a - j)) --> P (x) --> P (x + D) 
 ==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x+k*D))))
@@ -774,9 +776,8 @@
   done
 
 
-(*=============================================================================*)
-
-(*Theorems for the quantifier elminination Functions.*)
+text {*
+  \bigskip Theorems for the quantifier elminination Functions. *}
 
 lemma qe_ex_conj: "(EX (x::int). A x) = R
 		==> (EX (x::int). P x) = (Q & (EX x::int. A x))
@@ -805,7 +806,7 @@
 lemma qe_ALL: "(EX x. ~P x) = R ==> (ALL x. P x) = (~R)"
 by blast
 
-(* Theorems for proving NNF *)
+text {* \bigskip Theorems for proving NNF *}
 
 lemma nnf_im: "((~P) = P1) ==> (Q=Q1) ==> ((P --> Q) = (P1 | Q1))"
 by blast
@@ -851,7 +852,7 @@
 apply(fastsimp)
 done
 
-(* Theorems required for the adjustcoeffitienteq*)
+text {* \bigskip Theorems required for the @{text adjustcoeffitienteq} *}
 
 lemma ac_dvd_eq: assumes not0: "0 ~= (k::int)"
 shows "((m::int) dvd (c*n+t)) = (k*m dvd ((k*c)*n+(k*t)))" (is "?P = ?Q")
@@ -925,7 +926,7 @@
 lemma lf_dvd: "(l::int) = ll ==> (r::int) = lr ==> (l dvd r) =(ll dvd lr)"
 by simp
 
-(* Theorems for transforming predicates on nat to predicates on int*)
+text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*}
 
 theorem all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))"
   by (simp split add: split_nat)
@@ -973,7 +974,9 @@
 
 theorem Suc_plus1: "Suc n = n + 1" by simp
 
-(* specific instances of congruence rules, to prevent simplifier from looping *)
+text {*
+  \medskip Specific instances of congruence rules, to prevent
+  simplifier from looping. *}
 
 theorem imp_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::nat) \<longrightarrow> P) = (0 <= x \<longrightarrow> P')"
   by simp
diff -r 37a92211a5d3 -r dbb95b825244 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Fri Apr 16 04:06:52 2004 +0200
+++ b/src/HOL/Power.thy	Fri Apr 16 04:07:10 2004 +0200
@@ -24,7 +24,7 @@
 
 lemma power_one [simp]: "1^n = (1::'a::ringpower)"
 apply (induct_tac "n")
-apply (auto simp add: power_Suc)  
+apply (auto simp add: power_Suc)
 done
 
 lemma power_one_right [simp]: "(a::'a::ringpower) ^ 1 = a"
@@ -41,7 +41,7 @@
 done
 
 lemma power_mult_distrib: "((a::'a::ringpower) * b) ^ n = (a^n) * (b^n)"
-apply (induct_tac "n") 
+apply (induct_tac "n")
 apply (auto simp add: power_Suc mult_ac)
 done
 
@@ -54,7 +54,7 @@
 lemma zero_le_power:
      "0 \<le> (a::'a::{ordered_semiring,ringpower}) ==> 0 \<le> a^n"
 apply (simp add: order_le_less)
-apply (erule disjE) 
+apply (erule disjE)
 apply (simp_all add: zero_less_power zero_less_one power_0_left)
 done
 
@@ -62,25 +62,22 @@
      "1 \<le> (a::'a::{ordered_semiring,ringpower}) ==> 1 \<le> a^n"
 apply (induct_tac "n")
 apply (simp_all add: power_Suc)
-apply (rule order_trans [OF _ mult_mono [of 1 _ 1]]) 
-apply (simp_all add: zero_le_one order_trans [OF zero_le_one]) 
+apply (rule order_trans [OF _ mult_mono [of 1 _ 1]])
+apply (simp_all add: zero_le_one order_trans [OF zero_le_one])
 done
 
 lemma gt1_imp_ge0: "1 < a ==> 0 \<le> (a::'a::ordered_semiring)"
   by (simp add: order_trans [OF zero_le_one order_less_imp_le])
 
 lemma power_gt1_lemma:
-     assumes gt1: "1 < (a::'a::{ordered_semiring,ringpower})"
-        shows     "1 < a * a^n"
+  assumes gt1: "1 < (a::'a::{ordered_semiring,ringpower})"
+  shows "1 < a * a^n"
 proof -
-  have "1*1 < a * a^n"
-    proof (rule order_less_le_trans) 
-      show "1*1 < a*1" by (simp add: gt1)
-      show  "a*1 \<le> a * a^n"
-   by (simp only: mult_mono gt1 gt1_imp_ge0 one_le_power order_less_imp_le 
-                  zero_le_one order_refl)
-    qed
-  thus ?thesis by simp
+  have "1*1 < a*1" using gt1 by simp
+  also have "\<dots> \<le> a * a^n" using gt1
+    by (simp only: mult_mono gt1_imp_ge0 one_le_power order_less_imp_le
+        zero_le_one order_refl)
+  finally show ?thesis by simp
 qed
 
 lemma power_gt1:
@@ -88,52 +85,52 @@
 by (simp add: power_gt1_lemma power_Suc)
 
 lemma power_le_imp_le_exp:
-     assumes gt1: "(1::'a::{ringpower,ordered_semiring}) < a"
-       shows      "!!n. a^m \<le> a^n ==> m \<le> n"
-proof (induct "m")
+  assumes gt1: "(1::'a::{ringpower,ordered_semiring}) < a"
+  shows "!!n. a^m \<le> a^n ==> m \<le> n"
+proof (induct m)
   case 0
-    show ?case by simp
+  show ?case by simp
 next
   case (Suc m)
-    show ?case 
-      proof (cases n)
-        case 0
-          from prems have "a * a^m \<le> 1" by (simp add: power_Suc)
-          with gt1 show ?thesis
-            by (force simp only: power_gt1_lemma 
-                                 linorder_not_less [symmetric])
-      next
-        case (Suc n)
-          from prems show ?thesis 
-	    by (force dest: mult_left_le_imp_le
-	          simp add: power_Suc order_less_trans [OF zero_less_one gt1]) 
-      qed
+  show ?case
+  proof (cases n)
+    case 0
+    from prems have "a * a^m \<le> 1" by (simp add: power_Suc)
+    with gt1 show ?thesis
+      by (force simp only: power_gt1_lemma
+          linorder_not_less [symmetric])
+  next
+    case (Suc n)
+    from prems show ?thesis
+      by (force dest: mult_left_le_imp_le
+          simp add: power_Suc order_less_trans [OF zero_less_one gt1])
+  qed
 qed
 
-text{*Surely we can strengthen this? It holds for 0<a<1 too.*}
+text{*Surely we can strengthen this? It holds for @{text "0<a<1"} too.*}
 lemma power_inject_exp [simp]:
      "1 < (a::'a::{ordered_semiring,ringpower}) ==> (a^m = a^n) = (m=n)"
-  by (force simp add: order_antisym power_le_imp_le_exp)  
+  by (force simp add: order_antisym power_le_imp_le_exp)
 
 text{*Can relax the first premise to @{term "0<a"} in the case of the
 natural numbers.*}
 lemma power_less_imp_less_exp:
      "[| (1::'a::{ringpower,ordered_semiring}) < a; a^m < a^n |] ==> m < n"
-by (simp add: order_less_le [of m n] order_less_le [of "a^m" "a^n"] 
-              power_le_imp_le_exp) 
+by (simp add: order_less_le [of m n] order_less_le [of "a^m" "a^n"]
+              power_le_imp_le_exp)
 
 
 lemma power_mono:
      "[|a \<le> b; (0::'a::{ringpower,ordered_semiring}) \<le> a|] ==> a^n \<le> b^n"
-apply (induct_tac "n") 
+apply (induct_tac "n")
 apply (simp_all add: power_Suc)
 apply (auto intro: mult_mono zero_le_power order_trans [of 0 a b])
 done
 
 lemma power_strict_mono [rule_format]:
-     "[|a < b; (0::'a::{ringpower,ordered_semiring}) \<le> a|] 
-      ==> 0 < n --> a^n < b^n" 
-apply (induct_tac "n") 
+     "[|a < b; (0::'a::{ringpower,ordered_semiring}) \<le> a|]
+      ==> 0 < n --> a^n < b^n"
+apply (induct_tac "n")
 apply (auto simp add: mult_strict_mono zero_le_power power_Suc
                       order_le_less_trans [of 0 a b])
 done
@@ -166,15 +163,15 @@
 apply (auto simp add: power_Suc inverse_mult_distrib)
 done
 
-lemma nonzero_power_divide: 
+lemma nonzero_power_divide:
     "b \<noteq> 0 ==> (a/b) ^ n = ((a::'a::{field,ringpower}) ^ n) / (b ^ n)"
 by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse)
 
-lemma power_divide: 
+lemma power_divide:
     "(a/b) ^ n = ((a::'a::{field,division_by_zero,ringpower}) ^ n / b ^ n)"
 apply (case_tac "b=0", simp add: power_0_left)
-apply (rule nonzero_power_divide) 
-apply assumption 
+apply (rule nonzero_power_divide)
+apply assumption
 done
 
 lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_ring,ringpower}) ^ n"
@@ -183,7 +180,7 @@
 done
 
 lemma zero_less_power_abs_iff [simp]:
-     "(0 < (abs a)^n) = (a \<noteq> (0::'a::{ordered_ring,ringpower}) | n=0)" 
+     "(0 < (abs a)^n) = (a \<noteq> (0::'a::{ordered_ring,ringpower}) | n=0)"
 proof (induct "n")
   case 0
     show ?case by (simp add: zero_less_one)
@@ -208,19 +205,19 @@
 lemma power_Suc_less:
      "[|(0::'a::{ordered_semiring,ringpower}) < a; a < 1|]
       ==> a * a^n < a^n"
-apply (induct_tac n) 
-apply (auto simp add: power_Suc mult_strict_left_mono) 
+apply (induct_tac n)
+apply (auto simp add: power_Suc mult_strict_left_mono)
 done
 
 lemma power_strict_decreasing:
      "[|n < N; 0 < a; a < (1::'a::{ordered_semiring,ringpower})|]
       ==> a^N < a^n"
-apply (erule rev_mp) 
-apply (induct_tac "N")  
-apply (auto simp add: power_Suc power_Suc_less less_Suc_eq) 
-apply (rename_tac m)  
+apply (erule rev_mp)
+apply (induct_tac "N")
+apply (auto simp add: power_Suc power_Suc_less less_Suc_eq)
+apply (rename_tac m)
 apply (subgoal_tac "a * a^m < 1 * a^n", simp)
-apply (rule mult_strict_mono) 
+apply (rule mult_strict_mono)
 apply (auto simp add: zero_le_power zero_less_one order_less_imp_le)
 done
 
@@ -228,47 +225,47 @@
 lemma power_decreasing:
      "[|n \<le> N; 0 \<le> a; a \<le> (1::'a::{ordered_semiring,ringpower})|]
       ==> a^N \<le> a^n"
-apply (erule rev_mp) 
-apply (induct_tac "N") 
-apply (auto simp add: power_Suc  le_Suc_eq) 
-apply (rename_tac m)  
+apply (erule rev_mp)
+apply (induct_tac "N")
+apply (auto simp add: power_Suc  le_Suc_eq)
+apply (rename_tac m)
 apply (subgoal_tac "a * a^m \<le> 1 * a^n", simp)
-apply (rule mult_mono) 
+apply (rule mult_mono)
 apply (auto simp add: zero_le_power zero_le_one)
 done
 
 lemma power_Suc_less_one:
      "[| 0 < a; a < (1::'a::{ordered_semiring,ringpower}) |] ==> a ^ Suc n < 1"
-apply (insert power_strict_decreasing [of 0 "Suc n" a], simp) 
+apply (insert power_strict_decreasing [of 0 "Suc n" a], simp)
 done
 
 text{*Proof again resembles that of @{text power_strict_decreasing}*}
 lemma power_increasing:
      "[|n \<le> N; (1::'a::{ordered_semiring,ringpower}) \<le> a|] ==> a^n \<le> a^N"
-apply (erule rev_mp) 
-apply (induct_tac "N") 
-apply (auto simp add: power_Suc le_Suc_eq) 
+apply (erule rev_mp)
+apply (induct_tac "N")
+apply (auto simp add: power_Suc le_Suc_eq)
 apply (rename_tac m)
 apply (subgoal_tac "1 * a^n \<le> a * a^m", simp)
-apply (rule mult_mono) 
+apply (rule mult_mono)
 apply (auto simp add: order_trans [OF zero_le_one] zero_le_power)
 done
 
 text{*Lemma for @{text power_strict_increasing}*}
 lemma power_less_power_Suc:
      "(1::'a::{ordered_semiring,ringpower}) < a ==> a^n < a * a^n"
-apply (induct_tac n) 
-apply (auto simp add: power_Suc mult_strict_left_mono order_less_trans [OF zero_less_one]) 
+apply (induct_tac n)
+apply (auto simp add: power_Suc mult_strict_left_mono order_less_trans [OF zero_less_one])
 done
 
 lemma power_strict_increasing:
      "[|n < N; (1::'a::{ordered_semiring,ringpower}) < a|] ==> a^n < a^N"
-apply (erule rev_mp) 
-apply (induct_tac "N")  
-apply (auto simp add: power_less_power_Suc power_Suc less_Suc_eq) 
+apply (erule rev_mp)
+apply (induct_tac "N")
+apply (auto simp add: power_less_power_Suc power_Suc less_Suc_eq)
 apply (rename_tac m)
 apply (subgoal_tac "1 * a^n < a * a^m", simp)
-apply (rule mult_strict_mono)  
+apply (rule mult_strict_mono)
 apply (auto simp add: order_less_trans [OF zero_less_one] zero_le_power
                  order_less_imp_le)
 done
@@ -282,13 +279,13 @@
    assume "~ a \<le> b"
    then have "b < a" by (simp only: linorder_not_le)
    then have "b ^ Suc n < a ^ Suc n"
-     by (simp only: prems power_strict_mono) 
+     by (simp only: prems power_strict_mono)
    from le and this show "False"
       by (simp add: linorder_not_less [symmetric])
  qed
-  
+
 lemma power_inject_base:
-     "[| a ^ Suc n = b ^ Suc n; 0 \<le> a; 0 \<le> b |] 
+     "[| a ^ Suc n = b ^ Suc n; 0 \<le> a; 0 \<le> b |]
       ==> a = (b::'a::{ordered_semiring,ringpower})"
 by (blast intro: power_le_imp_le_base order_antisym order_eq_refl sym)
 
@@ -298,7 +295,7 @@
 primrec (power)
   "p ^ 0 = 1"
   "p ^ (Suc n) = (p::nat) * (p ^ n)"
-  
+
 instance nat :: ringpower
 proof
   fix z n :: nat
@@ -321,7 +318,7 @@
 lemma nat_power_less_imp_less: "!!i::nat. [| 0 < i; i^m < i^n |] ==> m < n"
 apply (rule ccontr)
 apply (drule leI [THEN le_imp_power_dvd, THEN dvd_imp_le, THEN leD])
-apply (erule zero_less_power, auto) 
+apply (erule zero_less_power, auto)
 done
 
 lemma nat_zero_less_power_iff [simp]: "(0 < x^n) = (x \<noteq> (0::nat) | n=0)"
@@ -341,7 +338,7 @@
 
 subsection{*Binomial Coefficients*}
 
-text{*This development is based on the work of Andy Gordon and 
+text{*This development is based on the work of Andy Gordon and
 Florian Kammueller*}
 
 consts
@@ -400,7 +397,7 @@
 apply (induct_tac "n")
 apply (simp add: binomial_0, clarify)
 apply (case_tac "k")
-apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq 
+apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq
                       binomial_eq_0)
 done
 
@@ -408,7 +405,7 @@
   need to reason about division.*}
 lemma binomial_Suc_Suc_eq_times:
      "k \<le> n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k"
-by (simp add: Suc_times_binomial_eq div_mult_self_is_m zero_less_Suc 
+by (simp add: Suc_times_binomial_eq div_mult_self_is_m zero_less_Suc
         del: mult_Suc mult_Suc_right)
 
 text{*Another version, with -1 instead of Suc.*}
@@ -460,7 +457,7 @@
 val power_le_imp_le_base = thm"power_le_imp_le_base";
 val power_inject_base = thm"power_inject_base";
 *}
- 
+
 text{*ML bindings for the remaining theorems*}
 ML
 {*
diff -r 37a92211a5d3 -r dbb95b825244 src/HOL/PreList.thy
--- a/src/HOL/PreList.thy	Fri Apr 16 04:06:52 2004 +0200
+++ b/src/HOL/PreList.thy	Fri Apr 16 04:07:10 2004 +0200
@@ -6,13 +6,14 @@
 
 header{*A Basis for Building the Theory of Lists*}
 
-(*Is defined separately to serve as a basis for theory ToyList in the
-documentation.*)
-
 theory PreList =
     Wellfounded_Relations + Presburger + Recdef + Relation_Power + Parity:
 
-(*belongs to theory Wellfounded_Recursion*)
+text {*
+  Is defined separately to serve as a basis for theory ToyList in the
+  documentation. *}
+
 lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf]
+  -- {* belongs to theory @{text Wellfounded_Recursion} *}
 
 end
diff -r 37a92211a5d3 -r dbb95b825244 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Fri Apr 16 04:06:52 2004 +0200
+++ b/src/HOL/Presburger.thy	Fri Apr 16 04:07:10 2004 +0200
@@ -7,6 +7,8 @@
 generation for Cooper Algorithm  
 *)
 
+header {* Presburger Arithmetic: Cooper Algorithm *}
+
 theory Presburger = NatSimprocs + SetInterval
 files
   ("cooper_dec.ML")
@@ -14,7 +16,7 @@
   ("qelim.ML")
   ("presburger.ML"):
 
-(* Theorem for unitifying the coeffitients of x in an existential formula*)
+text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*}
 
 theorem unity_coeff_ex: "(\<exists>x::int. P (l * x)) = (\<exists>x. l dvd (1*x+0) \<and> P x)"
   apply (rule iffI)
@@ -54,7 +56,7 @@
 
 
 
-(*Theorems for the combination of proofs of the equality of P and P_m for integers x less than some integer z.*)
+text {*Theorems for the combination of proofs of the equality of @{text P} and @{text P_m} for integers @{text x} less than some integer @{text z}.*}
 
 theorem eq_minf_conjI: "\<exists>z1::int. \<forall>x. x < z1 \<longrightarrow> (A1 x = A2 x) \<Longrightarrow>
   \<exists>z2::int. \<forall>x. x < z2 \<longrightarrow> (B1 x = B2 x) \<Longrightarrow>
@@ -75,7 +77,7 @@
   done
 
 
-(*Theorems for the combination of proofs of the equality of P and P_m for integers x greather than some integer z.*)
+text {*Theorems for the combination of proofs of the equality of @{text P} and @{text P_m} for integers @{text x} greather than some integer @{text z}.*}
 
 theorem eq_pinf_conjI: "\<exists>z1::int. \<forall>x. z1 < x \<longrightarrow> (A1 x = A2 x) \<Longrightarrow>
   \<exists>z2::int. \<forall>x. z2 < x \<longrightarrow> (B1 x = B2 x) \<Longrightarrow>
@@ -93,75 +95,76 @@
   apply (rule_tac x = "max z1 z2" in exI)
   apply simp
   done
-(*=============================================================================*)
-(*Theorems for the combination of proofs of the modulo D property for P
-pluusinfinity*)
-(* FIXME : This is THE SAME theorem as for the minusinf version, but with +k.. instead of -k.. In the future replace these both with only one*)
+
+text {*
+  \medskip Theorems for the combination of proofs of the modulo @{text
+  D} property for @{text "P plusinfinity"}
+
+  FIXME: This is THE SAME theorem as for the @{text minusinf} version,
+  but with @{text "+k.."} instead of @{text "-k.."} In the future
+  replace these both with only one. *}
 
 theorem modd_pinf_conjI: "\<forall>(x::int) k. A x = A (x+k*d) \<Longrightarrow>
   \<forall>(x::int) k. B x = B (x+k*d) \<Longrightarrow>
   \<forall>(x::int) (k::int). (A x \<and> B x) = (A (x+k*d) \<and> B (x+k*d))"
   by simp
 
-
 theorem modd_pinf_disjI: "\<forall>(x::int) k. A x = A (x+k*d) \<Longrightarrow>
   \<forall>(x::int) k. B x = B (x+k*d) \<Longrightarrow>
   \<forall>(x::int) (k::int). (A x \<or> B x) = (A (x+k*d) \<or> B (x+k*d))"
   by simp
 
-(*=============================================================================*)
-(*This is one of the cases where the simplifed formula is prooved to habe some property
-(in relation to P_m) but we need to proove the property for the original formula (P_m)*)
-(*FIXME : This is exaclty the same thm as for minusinf.*)
+text {*
+  This is one of the cases where the simplifed formula is prooved to
+  habe some property (in relation to @{text P_m}) but we need to prove
+  the property for the original formula (@{text P_m})
+
+  FIXME: This is exaclty the same thm as for @{text minusinf}. *}
+
 lemma pinf_simp_eq: "ALL x. P(x) = Q(x) ==> (EX (x::int). P(x)) --> (EX (x::int). F(x))  ==> (EX (x::int). Q(x)) --> (EX (x::int). F(x)) "
-by blast
+  by blast
 
 
-
-(*=============================================================================*)
-(*Theorems for the combination of proofs of the modulo D property for P
-minusinfinity*)
+text {*
+  \medskip Theorems for the combination of proofs of the modulo @{text D}
+  property for @{text "P minusinfinity"} *}
 
 theorem modd_minf_conjI: "\<forall>(x::int) k. A x = A (x-k*d) \<Longrightarrow>
   \<forall>(x::int) k. B x = B (x-k*d) \<Longrightarrow>
   \<forall>(x::int) (k::int). (A x \<and> B x) = (A (x-k*d) \<and> B (x-k*d))"
   by simp
 
-
 theorem modd_minf_disjI: "\<forall>(x::int) k. A x = A (x-k*d) \<Longrightarrow>
   \<forall>(x::int) k. B x = B (x-k*d) \<Longrightarrow>
   \<forall>(x::int) (k::int). (A x \<or> B x) = (A (x-k*d) \<or> B (x-k*d))"
   by simp
 
-(*=============================================================================*)
-(*This is one of the cases where the simplifed formula is prooved to habe some property
-(in relation to P_m) but we need to proove the property for the original formula (P_m)*)
+text {*
+  This is one of the cases where the simplifed formula is prooved to
+  have some property (in relation to @{text P_m}) but we need to
+  prove the property for the original formula (@{text P_m}). *}
 
 lemma minf_simp_eq: "ALL x. P(x) = Q(x) ==> (EX (x::int). P(x)) --> (EX (x::int). F(x))  ==> (EX (x::int). Q(x)) --> (EX (x::int). F(x)) "
-by blast
+  by blast
 
-(*=============================================================================*)
-
-(*theorem needed for prooving at runtime divide properties using the arithmetic tatic
-(who knows only about modulo = 0)*)
+text {*
+  Theorem needed for proving at runtime divide properties using the
+  arithmetic tactic (which knows only about modulo = 0). *}
 
 lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
-by(simp add:dvd_def zmod_eq_0_iff)
-
-(*=============================================================================*)
+  by(simp add:dvd_def zmod_eq_0_iff)
 
-
-
-(*Theorems used for the combination of proof for the backwards direction of cooper's
-theorem. they rely exclusively on Predicate calculus.*)
+text {*
+  \medskip Theorems used for the combination of proof for the
+  backwards direction of Cooper's Theorem. They rely exclusively on
+  Predicate calculus.*}
 
 lemma not_ast_p_disjI: "(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> P1(x) --> P1(x + d))
 ==>
 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> P2(x) --> P2(x + d))
 ==>
 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) -->(P1(x) \<or> P2(x)) --> (P1(x + d) \<or> P2(x + d))) "
-by blast
-
+  by blast
 
 
 lemma not_ast_p_conjI: "(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a- j)) --> P1(x) --> P1(x + d))
@@ -170,18 +173,18 @@
 ==>
 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) -->(P1(x) \<and> P2(x)) --> (P1(x + d)
 \<and> P2(x + d))) "
-by blast
+  by blast
 
 lemma not_ast_p_Q_elim: "
 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) -->P(x) --> P(x + d))
 ==> ( P = Q )
 ==> (ALL x. ~(EX (j::int) : {1..d}. EX (a::int) : A. P(a - j)) -->P(x) --> P(x + d))"
-by blast
-(*=============================================================================*)
+  by blast
 
-
-(*Theorems used for the combination of proof for the backwards direction of cooper's
-theorem. they rely exclusively on Predicate calculus.*)
+text {*
+  \medskip Theorems used for the combination of proof for the
+  backwards direction of Cooper's Theorem. They rely exclusively on
+  Predicate calculus.*}
 
 lemma not_bst_p_disjI: "(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> P1(x) --> P1(x - d))
 ==>
@@ -189,9 +192,7 @@
 ==>
 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) -->(P1(x) \<or> P2(x)) --> (P1(x - d)
 \<or> P2(x-d))) "
-by blast
-
-
+  by blast
 
 lemma not_bst_p_conjI: "(ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> P1(x) --> P1(x - d))
 ==>
@@ -199,68 +200,67 @@
 ==>
 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) -->(P1(x) \<and> P2(x)) --> (P1(x - d)
 \<and> P2(x-d))) "
-by blast
+  by blast
 
 lemma not_bst_p_Q_elim: "
 (ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) -->P(x) --> P(x - d)) 
 ==> ( P = Q )
 ==> (ALL x. ~(EX (j::int) : {1..d}. EX (b::int) : B. P(b+j)) -->P(x) --> P(x - d))"
-by blast
-(*=============================================================================*)
+  by blast
 
-(*This is the first direction of cooper's theorem*)
+text {* \medskip This is the first direction of Cooper's Theorem. *}
 lemma cooper_thm: "(R --> (EX x::int. P x))  ==> (Q -->(EX x::int.  P x )) ==> ((R|Q) --> (EX x::int. P x )) "
-by blast
+  by blast
 
-(*=============================================================================*)
-(*The full cooper's theoorem in its equivalence Form- Given the premisses it is trivial
-too, it relies exclusively on prediacte calculus.*)
+text {*
+  \medskip The full Cooper's Theorem in its equivalence Form. Given
+  the premises it is trivial too, it relies exclusively on prediacte calculus.*}
 lemma cooper_eq_thm: "(R --> (EX x::int. P x))  ==> (Q -->(EX x::int.  P x )) ==> ((~Q)
 --> (EX x::int. P x ) --> R) ==> (EX x::int. P x) = R|Q "
-by blast
+  by blast
 
-(*=============================================================================*)
-(*Some of the atomic theorems generated each time the atom does not depend on x, they
-are trivial.*)
+text {*
+  \medskip Some of the atomic theorems generated each time the atom
+  does not depend on @{text x}, they are trivial.*}
 
 lemma  fm_eq_minf: "EX z::int. ALL x. x < z --> (P = P) "
-by blast
+  by blast
 
 lemma  fm_modd_minf: "ALL (x::int). ALL (k::int). (P = P)"
-by blast
+  by blast
 
 lemma not_bst_p_fm: "ALL (x::int). Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> fm --> fm"
-by blast
-
-
+  by blast
 
 lemma  fm_eq_pinf: "EX z::int. ALL x. z < x --> (P = P) "
-by blast
+  by blast
 
-(* The next 2 thms are the same as the minusinf version*)
+text {* The next two thms are the same as the @{text minusinf} version. *}
+
 lemma  fm_modd_pinf: "ALL (x::int). ALL (k::int). (P = P)"
-by blast
+  by blast
 
 lemma not_ast_p_fm: "ALL (x::int). Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> fm --> fm"
-by blast
+  by blast
 
+text {* Theorems to be deleted from simpset when proving simplified formulaes. *}
 
-(* Theorems to be deleted from simpset when proving simplified formulaes*)
 lemma P_eqtrue: "(P=True) = P"
   by rules
 
 lemma P_eqfalse: "(P=False) = (~P)"
   by rules
 
-(*=============================================================================*)
+text {*
+  \medskip Theorems for the generation of the bachwards direction of
+  Cooper's Theorem.
 
-(*Theorems for the generation of the bachwards direction of cooper's theorem*)
-(*These are the 6 interesting atomic cases which have to be proved relying on the
-properties of B-set ant the arithmetic and contradiction proofs*)
+  These are the 6 interesting atomic cases which have to be proved relying on the
+  properties of B-set and the arithmetic and contradiction proofs. *}
 
 lemma not_bst_p_lt: "0 < (d::int) ==>
  ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> ( 0 < -x + a) --> (0 < -(x - d) + a )"
-by arith
+  by arith
 
 lemma not_bst_p_gt: "\<lbrakk> (g::int) \<in> B; g = -a \<rbrakk> \<Longrightarrow>
  ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (b::int) : B. Q(b+j)) --> (0 < (x) + a) --> ( 0 < (x - d) + a)"
@@ -315,16 +315,17 @@
 apply(simp add:int_distrib)
 done
 
-
+text {*
+  \medskip Theorems for the generation of the bachwards direction of
+  Cooper's Theorem.
 
-(*Theorems for the generation of the bachwards direction of cooper's theorem*)
-(*These are the 6 interesting atomic cases which have to be proved relying on the
-properties of A-set ant the arithmetic and contradiction proofs*)
+  These are the 6 interesting atomic cases which have to be proved
+  relying on the properties of A-set ant the arithmetic and
+  contradiction proofs. *}
 
 lemma not_ast_p_gt: "0 < (d::int) ==>
  ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> ( 0 < x + t) --> (0 < (x + d) + t )"
-by arith
-
+  by arith
 
 lemma not_ast_p_lt: "\<lbrakk>0 < d ;(t::int) \<in> A \<rbrakk> \<Longrightarrow>
  ALL x. Q(x::int) \<and> ~(EX (j::int) : {1..d}. EX (a::int) : A. Q(a - j)) --> (0 < -x + t) --> ( 0 < -(x + d) + t)"
@@ -377,12 +378,11 @@
   apply(simp add:int_distrib)
   done
 
-
+text {*
+  \medskip These are the atomic cases for the proof generation for the
+  modulo @{text D} property for @{text "P plusinfinity"}
 
-(*=============================================================================*)
-(*These are the atomic cases for the proof generation for the modulo D property for P
-plusinfinity*)
-(*They are fully based on arithmetics*)
+  They are fully based on arithmetics. *}
 
 lemma  dvd_modd_pinf: "((d::int) dvd d1) ==>
  (ALL (x::int). ALL (k::int). (((d::int) dvd (x + t)) = (d dvd (x+k*d1 + t))))"
@@ -412,10 +412,12 @@
   apply(simp add:int_distrib mult_ac)
   done
 
-(*=============================================================================*)
-(*These are the atomic cases for the proof generation for the equivalence of P and P
-plusinfinity for integers x greather than some integer z.*)
-(*They are fully based on arithmetics*)
+text {*
+  \medskip These are the atomic cases for the proof generation for the
+  equivalence of @{text P} and @{text "P plusinfinity"} for integers
+  @{text x} greater than some integer @{text z}.
+
+  They are fully based on arithmetics. *}
 
 lemma  eq_eq_pinf: "EX z::int. ALL x. z < x --> (( 0 = x +t ) = False )"
   apply(rule_tac x = "-t" in exI)
@@ -438,18 +440,16 @@
   done
 
 lemma  dvd_eq_pinf: "EX z::int. ALL x.  z < x --> ((d dvd (x + t)) = (d dvd (x + t))) "
-by simp
+  by simp
 
 lemma  not_dvd_eq_pinf: "EX z::int. ALL x. z < x  --> ((~(d dvd (x + t))) = (~(d dvd (x + t)))) "
-by simp
-
-
-
+  by simp
 
-(*=============================================================================*)
-(*These are the atomic cases for the proof generation for the modulo D property for P
-minusinfinity*)
-(*They are fully based on arithmetics*)
+text {*
+  \medskip These are the atomic cases for the proof generation for the
+  modulo @{text D} property for @{text "P minusinfinity"}.
+
+  They are fully based on arithmetics. *}
 
 lemma  dvd_modd_minf: "((d::int) dvd d1) ==>
  (ALL (x::int). ALL (k::int). (((d::int) dvd (x + t)) = (d dvd (x-k*d1 + t))))"
@@ -480,11 +480,12 @@
 apply(simp add:int_distrib mult_ac)
 done
 
+text {*
+  \medskip These are the atomic cases for the proof generation for the
+  equivalence of @{text P} and @{text "P minusinfinity"} for integers
+  @{text x} less than some integer @{text z}.
 
-(*=============================================================================*)
-(*These are the atomic cases for the proof generation for the equivalence of P and P
-minusinfinity for integers x less than some integer z.*)
-(*They are fully based on arithmetics*)
+  They are fully based on arithmetics. *}
 
 lemma  eq_eq_minf: "EX z::int. ALL x. x < z --> (( 0 = x +t ) = False )"
 apply(rule_tac x = "-t" in exI)
@@ -508,17 +509,18 @@
 done
 
 lemma  dvd_eq_minf: "EX z::int. ALL x. x < z --> ((d dvd (x + t)) = (d dvd (x + t))) "
-by simp
+  by simp
 
 lemma  not_dvd_eq_minf: "EX z::int. ALL x. x < z --> ((~(d dvd (x + t))) = (~(d dvd (x + t)))) "
-by simp
-
+  by simp
 
-(*=============================================================================*)
-(*This Theorem combines whithnesses about P minusinfinity to schow one component of the
-equivalence proof for cooper's theorem*)
+text {*
+  \medskip This Theorem combines whithnesses about @{text "P
+  minusinfinity"} to show one component of the equivalence proof for
+  Cooper's Theorem.
 
-(* FIXME: remove once they are part of the distribution *)
+  FIXME: remove once they are part of the distribution. *}
+
 theorem int_ge_induct[consumes 1,case_names base step]:
   assumes ge: "k \<le> (i::int)" and
         base: "P(k)" and
@@ -590,9 +592,10 @@
   qed
 qed
 
-(*=============================================================================*)
-(*This Theorem combines whithnesses about P minusinfinity to schow one component of the
-equivalence proof for cooper's theorem*)
+text {*
+  \medskip This Theorem combines whithnesses about @{text "P
+  minusinfinity"} to show one component of the equivalence proof for
+  Cooper's Theorem. *}
 
 lemma plusinfinity:
   assumes "0 < d" and
@@ -613,10 +616,8 @@
   qed
 qed
  
-
-
-(*=============================================================================*)
-(*Theorem for periodic function on discrete sets*)
+text {*
+  \medskip Theorem for periodic function on discrete sets. *}
 
 lemma minf_vee:
   assumes dpos: "(0::int) < d" and modd: "ALL x k. P x = P(x - k*d)"
@@ -651,8 +652,9 @@
   assume ?RHS thus ?LHS by blast
 qed
 
-(*=============================================================================*)
-(*Theorem for periodic function on discrete sets*)
+text {*
+  \medskip Theorem for periodic function on discrete sets. *}
+
 lemma pinf_vee:
   assumes dpos: "0 < (d::int)" and modd: "ALL (x::int) (k::int). P x = P (x+k*d)"
   shows "(EX x::int. P x) = (EX (j::int) : {1..d} . P j)"
@@ -750,7 +752,7 @@
 apply(blast dest:decr_mult_lemma)
 done
 
-(* Cooper Thm `, plus infinity version*)
+text {* Cooper Theorem, plus infinity version. *}
 lemma cppi_eq: "0 < D \<Longrightarrow> (EX z::int. ALL x. z < x --> (P x = P1 x))
 ==> ALL x.~(EX (j::int) : {1..D}. EX (a::int) : A. P(a - j)) --> P (x) --> P (x + D) 
 ==> (ALL (x::int). ALL (k::int). ((P1 x)= (P1 (x+k*D))))
@@ -774,9 +776,8 @@
   done
 
 
-(*=============================================================================*)
-
-(*Theorems for the quantifier elminination Functions.*)
+text {*
+  \bigskip Theorems for the quantifier elminination Functions. *}
 
 lemma qe_ex_conj: "(EX (x::int). A x) = R
 		==> (EX (x::int). P x) = (Q & (EX x::int. A x))
@@ -805,7 +806,7 @@
 lemma qe_ALL: "(EX x. ~P x) = R ==> (ALL x. P x) = (~R)"
 by blast
 
-(* Theorems for proving NNF *)
+text {* \bigskip Theorems for proving NNF *}
 
 lemma nnf_im: "((~P) = P1) ==> (Q=Q1) ==> ((P --> Q) = (P1 | Q1))"
 by blast
@@ -851,7 +852,7 @@
 apply(fastsimp)
 done
 
-(* Theorems required for the adjustcoeffitienteq*)
+text {* \bigskip Theorems required for the @{text adjustcoeffitienteq} *}
 
 lemma ac_dvd_eq: assumes not0: "0 ~= (k::int)"
 shows "((m::int) dvd (c*n+t)) = (k*m dvd ((k*c)*n+(k*t)))" (is "?P = ?Q")
@@ -925,7 +926,7 @@
 lemma lf_dvd: "(l::int) = ll ==> (r::int) = lr ==> (l dvd r) =(ll dvd lr)"
 by simp
 
-(* Theorems for transforming predicates on nat to predicates on int*)
+text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*}
 
 theorem all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))"
   by (simp split add: split_nat)
@@ -973,7 +974,9 @@
 
 theorem Suc_plus1: "Suc n = n + 1" by simp
 
-(* specific instances of congruence rules, to prevent simplifier from looping *)
+text {*
+  \medskip Specific instances of congruence rules, to prevent
+  simplifier from looping. *}
 
 theorem imp_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::nat) \<longrightarrow> P) = (0 <= x \<longrightarrow> P')"
   by simp
diff -r 37a92211a5d3 -r dbb95b825244 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Fri Apr 16 04:06:52 2004 +0200
+++ b/src/HOL/SetInterval.thy	Fri Apr 16 04:07:10 2004 +0200
@@ -7,6 +7,8 @@
 lessThan, greaterThan, atLeast, atMost and two-sided intervals
 *)
 
+header {* Set intervals *}
+
 theory SetInterval = IntArith:
 
 constdefs
@@ -145,33 +147,33 @@
 
 subsection {*Two-sided intervals*}
 
-(* greaterThanLessThan *)
+text {* @{text greaterThanLessThan} *}
 
 lemma greaterThanLessThan_iff [simp]:
   "(i : {)l..u(}) = (l < i & i < u)"
 by (simp add: greaterThanLessThan_def)
 
-(* atLeastLessThan *)
+text {* @{text atLeastLessThan} *}
 
 lemma atLeastLessThan_iff [simp]:
   "(i : {l..u(}) = (l <= i & i < u)"
 by (simp add: atLeastLessThan_def)
 
-(* greaterThanAtMost *)
+text {* @{text greaterThanAtMost} *}
 
 lemma greaterThanAtMost_iff [simp]:
   "(i : {)l..u}) = (l < i & i <= u)"
 by (simp add: greaterThanAtMost_def)
 
-(* atLeastAtMost *)
+text {* @{text atLeastAtMost} *}
 
 lemma atLeastAtMost_iff [simp]:
   "(i : {l..u}) = (l <= i & i <= u)"
 by (simp add: atLeastAtMost_def)
 
-(* The above four lemmas could be declared as iffs.
-   If we do so, a call to blast in Hyperreal/Star.ML, lemma STAR_Int
-   seems to take forever (more than one hour). *)
+text {* The above four lemmas could be declared as iffs.
+  If we do so, a call to blast in Hyperreal/Star.ML, lemma @{text STAR_Int}
+  seems to take forever (more than one hour). *}
 
 
 subsection {* Intervals of natural numbers *}
@@ -227,7 +229,7 @@
 lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"
 by blast
 
-(* Intervals of nats with Suc *)
+text {* Intervals of nats with @{text Suc} *}
 
 lemma atLeastLessThanSuc_atLeastAtMost: "{l..Suc u(} = {l..u}"
   by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def)
@@ -391,11 +393,11 @@
 
 subsection {*Lemmas useful with the summation operator setsum*}
 
-(* For examples, see Algebra/poly/UnivPoly.thy *)
+text {* For examples, see Algebra/poly/UnivPoly.thy *}
 
-(** Disjoint Unions **)
+subsubsection {* Disjoint Unions *}
 
-(* Singletons and open intervals *)
+text {* Singletons and open intervals *}
 
 lemma ivl_disj_un_singleton:
   "{l::'a::linorder} Un {)l..} = {l..}"
@@ -406,7 +408,7 @@
   "(l::'a::linorder) <= u ==> {l..u(} Un {u} = {l..u}"
 by auto
 
-(* One- and two-sided intervals *)
+text {* One- and two-sided intervals *}
 
 lemma ivl_disj_un_one:
   "(l::'a::linorder) < u ==> {..l} Un {)l..u(} = {..u(}"
@@ -419,7 +421,7 @@
   "(l::'a::linorder) <= u ==> {l..u(} Un {u..} = {l..}"
 by auto
 
-(* Two- and two-sided intervals *)
+text {* Two- and two-sided intervals *}
 
 lemma ivl_disj_un_two:
   "[| (l::'a::linorder) < m; m <= u |] ==> {)l..m(} Un {m..u(} = {)l..u(}"
@@ -434,9 +436,9 @@
 
 lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two
 
-(** Disjoint Intersections **)
+subsubsection {* Disjoint Intersections *}
 
-(* Singletons and open intervals *)
+text {* Singletons and open intervals *}
 
 lemma ivl_disj_int_singleton:
   "{l::'a::order} Int {)l..} = {}"
@@ -447,7 +449,7 @@
   "{l..u(} Int {u} = {}"
   by simp+
 
-(* One- and two-sided intervals *)
+text {* One- and two-sided intervals *}
 
 lemma ivl_disj_int_one:
   "{..l::'a::order} Int {)l..u(} = {}"
@@ -460,7 +462,7 @@
   "{l..u(} Int {u..} = {}"
   by auto
 
-(* Two- and two-sided intervals *)
+text {* Two- and two-sided intervals *}
 
 lemma ivl_disj_int_two:
   "{)l::'a::order..m(} Int {m..u(} = {}"