--- 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
--- 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
--- 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"
--- 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
--- 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