tuned document;
authorwenzelm
Fri Apr 16 13:51:04 2004 +0200 (2004-04-16)
changeset 14589feae7b5fd425
parent 14588 29311d81954e
child 14590 276ef51cedbf
tuned document;
src/HOL/Library/Library/document/root.tex
src/HOL/Library/While_Combinator.thy
src/HOL/Library/Word.thy
src/HOL/List.thy
src/HOL/Refute.thy
     1.1 --- a/src/HOL/Library/Library/document/root.tex	Fri Apr 16 12:09:31 2004 +0200
     1.2 +++ b/src/HOL/Library/Library/document/root.tex	Fri Apr 16 13:51:04 2004 +0200
     1.3 @@ -19,6 +19,8 @@
     1.4    David von Oheimb \\
     1.5    Lawrence C Paulson \\
     1.6    Thomas M Rasmussen \\
     1.7 +  Stefan Richter \\
     1.8 +  Sebastian Skalberg \\
     1.9    Christophe Tabacznyj \\
    1.10    Markus Wenzel}
    1.11  \maketitle
     2.1 --- a/src/HOL/Library/While_Combinator.thy	Fri Apr 16 12:09:31 2004 +0200
     2.2 +++ b/src/HOL/Library/While_Combinator.thy	Fri Apr 16 13:51:04 2004 +0200
     2.3 @@ -141,12 +141,11 @@
     2.4  
     2.5  
     2.6  text {*
     2.7 - An example of using the @{term while} combinator.\footnote{It is safe
     2.8 - to keep the example here, since there is no effect on the current
     2.9 - theory.}
    2.10 + An example of using the @{term while} combinator.
    2.11  *}
    2.12  
    2.13 -theorem "P (lfp (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6 | n. n \<in> N})) = P {0, 4, 2}"
    2.14 +theorem "P (lfp (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6 | n. n \<in> N})) =
    2.15 +  P {0, 4, 2}"
    2.16  proof -
    2.17    have aux: "!!f A B. {f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}"
    2.18      apply blast
     3.1 --- a/src/HOL/Library/Word.thy	Fri Apr 16 12:09:31 2004 +0200
     3.2 +++ b/src/HOL/Library/Word.thy	Fri Apr 16 13:51:04 2004 +0200
     3.3 @@ -3,6 +3,11 @@
     3.4      Author:     Sebastian Skalberg (TU Muenchen)
     3.5  *)
     3.6  
     3.7 +header {*
     3.8 +  \title{Binary Words}
     3.9 +  \author{Sebastian Skalberg}
    3.10 +*}
    3.11 +
    3.12  theory Word = Main files "word_setup.ML":
    3.13  
    3.14  subsection {* Auxilary Lemmas *}
    3.15 @@ -235,7 +240,7 @@
    3.16  lemma int_nat_two_exp: "2 ^ k = int (2 ^ k)"
    3.17    by (induct k,simp_all)
    3.18  
    3.19 -section {* Bits *}
    3.20 +subsection {* Bits *}
    3.21  
    3.22  datatype bit
    3.23    = Zero ("\<zero>")
    3.24 @@ -294,7 +299,7 @@
    3.25  lemma [simp]: "(b bitxor b) = \<zero>"
    3.26    by (cases b,simp_all)
    3.27  
    3.28 -section {* Bit Vectors *}
    3.29 +subsection {* Bit Vectors *}
    3.30  
    3.31  text {* First, a couple of theorems expressing case analysis and
    3.32  induction principles for bit vectors. *}
    3.33 @@ -1144,7 +1149,7 @@
    3.34      by simp
    3.35  qed
    3.36  
    3.37 -section {* Unsigned Arithmetic Operations *}
    3.38 +subsection {* Unsigned Arithmetic Operations *}
    3.39  
    3.40  constdefs
    3.41    bv_add :: "[bit list, bit list ] => bit list"
    3.42 @@ -1240,7 +1245,7 @@
    3.43      by arith
    3.44  qed
    3.45  
    3.46 -section {* Signed Vectors *}
    3.47 +subsection {* Signed Vectors *}
    3.48  
    3.49  consts
    3.50    norm_signed :: "bit list => bit list"
    3.51 @@ -1909,9 +1914,9 @@
    3.52      by simp
    3.53  qed
    3.54  
    3.55 -section {* Signed Arithmetic Operations *}
    3.56 +subsection {* Signed Arithmetic Operations *}
    3.57  
    3.58 -subsection {* Conversion from unsigned to signed *}
    3.59 +subsubsection {* Conversion from unsigned to signed *}
    3.60  
    3.61  constdefs
    3.62    utos :: "bit list => bit list"
    3.63 @@ -1935,7 +1940,7 @@
    3.64      by simp
    3.65  qed
    3.66  
    3.67 -subsection {* Unary minus *}
    3.68 +subsubsection {* Unary minus *}
    3.69  
    3.70  constdefs
    3.71    bv_uminus :: "bit list => bit list"
    3.72 @@ -2546,7 +2551,7 @@
    3.73  lemma bv_smult_sym: "bv_smult w1 w2 = bv_smult w2 w1"
    3.74    by (simp add: bv_smult_def zmult_ac)
    3.75  
    3.76 -section {* Structural operations *}
    3.77 +subsection {* Structural operations *}
    3.78  
    3.79  constdefs
    3.80    bv_select :: "[bit list,nat] => bit"
     4.1 --- a/src/HOL/List.thy	Fri Apr 16 12:09:31 2004 +0200
     4.2 +++ b/src/HOL/List.thy	Fri Apr 16 13:51:04 2004 +0200
     4.3 @@ -76,7 +76,7 @@
     4.4  
     4.5  
     4.6  text {*
     4.7 -  Function @{text size} is overloaded for all datatypes.Users may
     4.8 +  Function @{text size} is overloaded for all datatypes. Users may
     4.9    refer to the list version as @{text length}. *}
    4.10  
    4.11  syntax length :: "'a list => nat"
    4.12 @@ -795,7 +795,6 @@
    4.13  by(simp add:last_append)
    4.14  
    4.15  
    4.16 -
    4.17  lemma length_butlast [simp]: "length (butlast xs) = length xs - 1"
    4.18  by (induct xs rule: rev_induct) auto
    4.19  
     5.1 --- a/src/HOL/Refute.thy	Fri Apr 16 12:09:31 2004 +0200
     5.2 +++ b/src/HOL/Refute.thy	Fri Apr 16 13:51:04 2004 +0200
     5.3 @@ -6,6 +6,25 @@
     5.4  Basic setup and documentation for the 'refute' (and 'refute_params') command.
     5.5  *)
     5.6  
     5.7 +header {* Refute *}
     5.8 +
     5.9 +theory Refute = Map
    5.10 +
    5.11 +files "Tools/prop_logic.ML"
    5.12 +      "Tools/sat_solver.ML"
    5.13 +      "Tools/refute.ML"
    5.14 +      "Tools/refute_isar.ML":
    5.15 +
    5.16 +use "Tools/prop_logic.ML"
    5.17 +use "Tools/sat_solver.ML"
    5.18 +use "Tools/refute.ML"
    5.19 +use "Tools/refute_isar.ML"
    5.20 +
    5.21 +setup Refute.setup
    5.22 +
    5.23 +text {*
    5.24 +\small
    5.25 +\begin{verbatim}
    5.26  (* ------------------------------------------------------------------------- *)
    5.27  (* REFUTE                                                                    *)
    5.28  (*                                                                           *)
    5.29 @@ -83,21 +102,7 @@
    5.30  (* HOL/Main.thy               Sets default parameters                        *)
    5.31  (* HOL/ex/RefuteExamples.thy  Examples                                       *)
    5.32  (* ------------------------------------------------------------------------- *)
    5.33 -
    5.34 -header {* Refute *}
    5.35 -
    5.36 -theory Refute = Map
    5.37 -
    5.38 -files "Tools/prop_logic.ML"
    5.39 -      "Tools/sat_solver.ML"
    5.40 -      "Tools/refute.ML"
    5.41 -      "Tools/refute_isar.ML":
    5.42 -
    5.43 -use "Tools/prop_logic.ML"
    5.44 -use "Tools/sat_solver.ML"
    5.45 -use "Tools/refute.ML"
    5.46 -use "Tools/refute_isar.ML"
    5.47 -
    5.48 -setup Refute.setup
    5.49 +\end{verbatim}
    5.50 +*}
    5.51  
    5.52  end