# HG changeset patch
# User wenzelm
# Date 1082116264 -7200
# Node ID feae7b5fd4257ccddbc59515104c4ee98c3ae3c7
# Parent  29311d81954ede58dcb286ea452bee6be7d8485c
tuned document;

diff -r 29311d81954e -r feae7b5fd425 src/HOL/Library/Library/document/root.tex
--- a/src/HOL/Library/Library/document/root.tex	Fri Apr 16 12:09:31 2004 +0200
+++ b/src/HOL/Library/Library/document/root.tex	Fri Apr 16 13:51:04 2004 +0200
@@ -19,6 +19,8 @@
   David von Oheimb \\
   Lawrence C Paulson \\
   Thomas M Rasmussen \\
+  Stefan Richter \\
+  Sebastian Skalberg \\
   Christophe Tabacznyj \\
   Markus Wenzel}
 \maketitle
diff -r 29311d81954e -r feae7b5fd425 src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Fri Apr 16 12:09:31 2004 +0200
+++ b/src/HOL/Library/While_Combinator.thy	Fri Apr 16 13:51:04 2004 +0200
@@ -141,12 +141,11 @@
 
 
 text {*
- An example of using the @{term while} combinator.\footnote{It is safe
- to keep the example here, since there is no effect on the current
- theory.}
+ An example of using the @{term while} combinator.
 *}
 
-theorem "P (lfp (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6 | n. n \<in> N})) = P {0, 4, 2}"
+theorem "P (lfp (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6 | n. n \<in> N})) =
+  P {0, 4, 2}"
 proof -
   have aux: "!!f A B. {f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}"
     apply blast
diff -r 29311d81954e -r feae7b5fd425 src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Fri Apr 16 12:09:31 2004 +0200
+++ b/src/HOL/Library/Word.thy	Fri Apr 16 13:51:04 2004 +0200
@@ -3,6 +3,11 @@
     Author:     Sebastian Skalberg (TU Muenchen)
 *)
 
+header {*
+  \title{Binary Words}
+  \author{Sebastian Skalberg}
+*}
+
 theory Word = Main files "word_setup.ML":
 
 subsection {* Auxilary Lemmas *}
@@ -235,7 +240,7 @@
 lemma int_nat_two_exp: "2 ^ k = int (2 ^ k)"
   by (induct k,simp_all)
 
-section {* Bits *}
+subsection {* Bits *}
 
 datatype bit
   = Zero ("\<zero>")
@@ -294,7 +299,7 @@
 lemma [simp]: "(b bitxor b) = \<zero>"
   by (cases b,simp_all)
 
-section {* Bit Vectors *}
+subsection {* Bit Vectors *}
 
 text {* First, a couple of theorems expressing case analysis and
 induction principles for bit vectors. *}
@@ -1144,7 +1149,7 @@
     by simp
 qed
 
-section {* Unsigned Arithmetic Operations *}
+subsection {* Unsigned Arithmetic Operations *}
 
 constdefs
   bv_add :: "[bit list, bit list ] => bit list"
@@ -1240,7 +1245,7 @@
     by arith
 qed
 
-section {* Signed Vectors *}
+subsection {* Signed Vectors *}
 
 consts
   norm_signed :: "bit list => bit list"
@@ -1909,9 +1914,9 @@
     by simp
 qed
 
-section {* Signed Arithmetic Operations *}
+subsection {* Signed Arithmetic Operations *}
 
-subsection {* Conversion from unsigned to signed *}
+subsubsection {* Conversion from unsigned to signed *}
 
 constdefs
   utos :: "bit list => bit list"
@@ -1935,7 +1940,7 @@
     by simp
 qed
 
-subsection {* Unary minus *}
+subsubsection {* Unary minus *}
 
 constdefs
   bv_uminus :: "bit list => bit list"
@@ -2546,7 +2551,7 @@
 lemma bv_smult_sym: "bv_smult w1 w2 = bv_smult w2 w1"
   by (simp add: bv_smult_def zmult_ac)
 
-section {* Structural operations *}
+subsection {* Structural operations *}
 
 constdefs
   bv_select :: "[bit list,nat] => bit"
diff -r 29311d81954e -r feae7b5fd425 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Apr 16 12:09:31 2004 +0200
+++ b/src/HOL/List.thy	Fri Apr 16 13:51:04 2004 +0200
@@ -76,7 +76,7 @@
 
 
 text {*
-  Function @{text size} is overloaded for all datatypes.Users may
+  Function @{text size} is overloaded for all datatypes. Users may
   refer to the list version as @{text length}. *}
 
 syntax length :: "'a list => nat"
@@ -795,7 +795,6 @@
 by(simp add:last_append)
 
 
-
 lemma length_butlast [simp]: "length (butlast xs) = length xs - 1"
 by (induct xs rule: rev_induct) auto
 
diff -r 29311d81954e -r feae7b5fd425 src/HOL/Refute.thy
--- a/src/HOL/Refute.thy	Fri Apr 16 12:09:31 2004 +0200
+++ b/src/HOL/Refute.thy	Fri Apr 16 13:51:04 2004 +0200
@@ -6,6 +6,25 @@
 Basic setup and documentation for the 'refute' (and 'refute_params') command.
 *)
 
+header {* Refute *}
+
+theory Refute = Map
+
+files "Tools/prop_logic.ML"
+      "Tools/sat_solver.ML"
+      "Tools/refute.ML"
+      "Tools/refute_isar.ML":
+
+use "Tools/prop_logic.ML"
+use "Tools/sat_solver.ML"
+use "Tools/refute.ML"
+use "Tools/refute_isar.ML"
+
+setup Refute.setup
+
+text {*
+\small
+\begin{verbatim}
 (* ------------------------------------------------------------------------- *)
 (* REFUTE                                                                    *)
 (*                                                                           *)
@@ -83,21 +102,7 @@
 (* HOL/Main.thy               Sets default parameters                        *)
 (* HOL/ex/RefuteExamples.thy  Examples                                       *)
 (* ------------------------------------------------------------------------- *)
-
-header {* Refute *}
-
-theory Refute = Map
-
-files "Tools/prop_logic.ML"
-      "Tools/sat_solver.ML"
-      "Tools/refute.ML"
-      "Tools/refute_isar.ML":
-
-use "Tools/prop_logic.ML"
-use "Tools/sat_solver.ML"
-use "Tools/refute.ML"
-use "Tools/refute_isar.ML"
-
-setup Refute.setup
+\end{verbatim}
+*}
 
 end