--- a/src/HOL/ex/CTL.thy Sun Jun 03 23:16:46 2007 +0200
+++ b/src/HOL/ex/CTL.thy Sun Jun 03 23:16:47 2007 +0200
@@ -80,7 +80,7 @@
lemmas [simp] = EX_def EG_def AX_def EF_def AF_def AG_def
-section {* Basic fixed point properties *}
+subsection {* Basic fixed point properties *}
text {*
First of all, we use the de-Morgan property of fixed points
@@ -187,7 +187,7 @@
by (simp only: AG_gfp) (rule gfp_upperbound)
-section {* The tree induction principle \label{sec:calc-ctl-tree-induct} *}
+subsection {* The tree induction principle \label{sec:calc-ctl-tree-induct} *}
text {*
With the most basic facts available, we are now able to establish a
@@ -283,7 +283,7 @@
qed
-section {* An application of tree induction \label{sec:calc-ctl-commute} *}
+subsection {* An application of tree induction \label{sec:calc-ctl-commute} *}
text {*
Further interesting properties of CTL expressions may be
--- a/src/HOL/ex/LocaleTest2.thy Sun Jun 03 23:16:46 2007 +0200
+++ b/src/HOL/ex/LocaleTest2.thy Sun Jun 03 23:16:47 2007 +0200
@@ -19,7 +19,8 @@
ML {* set show_hyps *}
ML {* set show_sorts *}
-section {* Interpretation of Defined Concepts *}
+
+subsection {* Interpretation of Defined Concepts *}
text {* Naming convention for global objects: prefixes D and d *}
--- a/src/HOL/ex/Refute_Examples.thy Sun Jun 03 23:16:46 2007 +0200
+++ b/src/HOL/ex/Refute_Examples.thy Sun Jun 03 23:16:47 2007 +0200
@@ -9,7 +9,6 @@
header {* Examples for the 'refute' command *}
theory Refute_Examples imports Main
-
begin
refute_params [satsolver="dpll"]
@@ -26,9 +25,9 @@
(******************************************************************************)
-section {* Examples and Test Cases *}
+subsection {* Examples and Test Cases *}
-subsection {* Propositional logic *}
+subsubsection {* Propositional logic *}
lemma "True"
refute
@@ -69,7 +68,7 @@
(******************************************************************************)
-subsection {* Predicate logic *}
+subsubsection {* Predicate logic *}
lemma "P x y z"
refute
@@ -85,7 +84,7 @@
(******************************************************************************)
-subsection {* Equality *}
+subsubsection {* Equality *}
lemma "P = True"
refute
@@ -119,7 +118,7 @@
(******************************************************************************)
-subsection {* First-Order Logic *}
+subsubsection {* First-Order Logic *}
lemma "\<exists>x. P x"
refute
@@ -213,7 +212,7 @@
(******************************************************************************)
-subsection {* Higher-Order Logic *}
+subsubsection {* Higher-Order Logic *}
lemma "\<exists>P. P"
refute
@@ -314,7 +313,7 @@
(******************************************************************************)
-subsection {* Meta-logic *}
+subsubsection {* Meta-logic *}
lemma "!!x. P x"
refute
@@ -346,7 +345,7 @@
(******************************************************************************)
-subsection {* Schematic variables *}
+subsubsection {* Schematic variables *}
lemma "?P"
refute
@@ -360,7 +359,7 @@
(******************************************************************************)
-subsection {* Abstractions *}
+subsubsection {* Abstractions *}
lemma "(\<lambda>x. x) = (\<lambda>x. y)"
refute
@@ -377,7 +376,7 @@
(******************************************************************************)
-subsection {* Sets *}
+subsubsection {* Sets *}
lemma "P (A::'a set)"
refute
@@ -422,7 +421,7 @@
(******************************************************************************)
-subsection {* arbitrary *}
+subsubsection {* arbitrary *}
lemma "arbitrary"
refute
@@ -442,7 +441,7 @@
(******************************************************************************)
-subsection {* The *}
+subsubsection {* The *}
lemma "The P"
refute
@@ -466,7 +465,7 @@
(******************************************************************************)
-subsection {* Eps *}
+subsubsection {* Eps *}
lemma "Eps P"
refute
@@ -491,7 +490,7 @@
(******************************************************************************)
-subsection {* Subtypes (typedef), typedecl *}
+subsubsection {* Subtypes (typedef), typedecl *}
text {* A completely unspecified non-empty subset of @{typ "'a"}: *}
@@ -513,7 +512,7 @@
(******************************************************************************)
-subsection {* Inductive datatypes *}
+subsubsection {* Inductive datatypes *}
text {* With @{text quick_and_dirty} set, the datatype package does
not generate certain axioms for recursion operators. Without these
@@ -521,7 +520,7 @@
ML {* reset quick_and_dirty *}
-subsubsection {* unit *}
+text {* unit *}
lemma "P (x::unit)"
refute
@@ -543,7 +542,7 @@
refute
oops
-subsubsection {* option *}
+text {* option *}
lemma "P (x::'a option)"
refute
@@ -569,7 +568,7 @@
refute
oops
-subsubsection {* * *}
+text {* * *}
lemma "P (x::'a*'b)"
refute
@@ -603,7 +602,7 @@
refute
oops
-subsubsection {* + *}
+text {* + *}
lemma "P (x::'a+'b)"
refute
@@ -633,7 +632,7 @@
refute
oops
-subsubsection {* Non-recursive datatypes *}
+text {* Non-recursive datatypes *}
datatype T1 = A | B
@@ -701,7 +700,7 @@
refute
oops
-subsubsection {* Recursive datatypes *}
+text {* Recursive datatypes *}
text {* nat *}
@@ -783,7 +782,7 @@
refute
oops
-subsubsection {* Mutually recursive datatypes *}
+text {* Mutually recursive datatypes *}
datatype 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp"
and 'a bexp = Equal "'a aexp" "'a aexp"
@@ -824,7 +823,7 @@
refute
oops
-subsubsection {* Other datatype examples *}
+text {* Other datatype examples *}
datatype Trie = TR "Trie list"
@@ -915,7 +914,7 @@
(******************************************************************************)
-subsection {* Records *}
+subsubsection {* Records *}
(*TODO: make use of pair types, rather than typedef, for record types*)
@@ -936,7 +935,7 @@
(******************************************************************************)
-subsection {* Inductively defined sets *}
+subsubsection {* Inductively defined sets *}
consts
arbitrarySet :: "'a set"
@@ -974,7 +973,7 @@
(******************************************************************************)
-subsection {* Examples involving special functions *}
+subsubsection {* Examples involving special functions *}
lemma "card x = 0"
refute
@@ -1026,7 +1025,7 @@
(******************************************************************************)
-subsection {* Axiomatic type classes and overloading *}
+subsubsection {* Axiomatic type classes and overloading *}
text {* A type class without axioms: *}
--- a/src/HOL/ex/Sudoku.thy Sun Jun 03 23:16:46 2007 +0200
+++ b/src/HOL/ex/Sudoku.thy Sun Jun 03 23:16:47 2007 +0200
@@ -7,9 +7,7 @@
header {* A SAT-based Sudoku Solver *}
theory Sudoku
-
imports Main
-
begin
text {*
--- a/src/HOL/ex/ThreeDivides.thy Sun Jun 03 23:16:46 2007 +0200
+++ b/src/HOL/ex/ThreeDivides.thy Sun Jun 03 23:16:47 2007 +0200
@@ -9,7 +9,7 @@
imports Main LaTeXsugar
begin
-section {* Abstract *}
+subsection {* Abstract *}
text {*
The following document presents a proof of the Three Divides N theorem
@@ -27,9 +27,10 @@
@{text "\<box>"}
*}
-section {* Formal proof *}
-subsection {* Miscellaneous summation lemmas *}
+subsection {* Formal proof *}
+
+subsubsection {* Miscellaneous summation lemmas *}
text {* If $a$ divides @{text "A x"} for all x then $a$ divides any
sum over terms of the form @{text "(A x)*(P x)"} for arbitrary $P$. *}
@@ -48,7 +49,8 @@
thus ?case by simp
qed
-subsection {* Generalised Three Divides *}
+
+subsubsection {* Generalised Three Divides *}
text {* This section solves a generalised form of the three divides
problem. Here we show that for any sequence of numbers the theorem
@@ -131,14 +133,15 @@
qed
-subsection {* Three Divides Natural *}
+subsubsection {* Three Divides Natural *}
text {* This section shows that for all natural numbers we can
generate a sequence of digits less than ten that represent the decimal
expansion of the number. We then use the lemma @{text
"three_div_general"} to prove our final theorem. *}
-subsubsection {* Definitions of length and digit sum *}
+
+text {* \medskip Definitions of length and digit sum. *}
text {* This section introduces some functions to calculate the
required properties of natural numbers. We then proceed to prove some
@@ -215,7 +218,7 @@
qed
-subsubsection {* Final theorem *}
+text {* \medskip Final theorem. *}
text {* We now combine the general theorem @{text "three_div_general"}
and existence result of @{text "exp_exists"} to prove our final
@@ -234,5 +237,4 @@
show "3 dvd n = (3 dvd (\<Sum>x<nlen n. n div 10^x mod 10))" by simp
qed
-
end
--- a/src/HOL/ex/Unification.thy Sun Jun 03 23:16:46 2007 +0200
+++ b/src/HOL/ex/Unification.thy Sun Jun 03 23:16:47 2007 +0200
@@ -4,9 +4,9 @@
header {* Case study: Unification Algorithm *}
-(*<*)theory Unification
+theory Unification
imports Main
-begin(*>*)
+begin
text {*
This is a formalization of a first-order unification
@@ -15,7 +15,7 @@
This is basically a modernized version of a previous formalization
by Konrad Slind (see: HOL/Subst/Unify.thy), which itself builds on
- previous work by Paulson and Manna @{text "&"} Waldinger (for details, see
+ previous work by Paulson and Manna \& Waldinger (for details, see
there).
Unlike that formalization, where the proofs of termination and
@@ -23,6 +23,7 @@
partial correctness and termination separately.
*}
+
subsection {* Basic definitions *}
datatype 'a trm =
@@ -62,6 +63,7 @@
where
"s1 =\<^sub>s s2 \<equiv> \<forall>t. t \<triangleleft> s1 = t \<triangleleft> s2"
+
subsection {* Basic lemmas *}
lemma apply_empty[simp]: "t \<triangleleft> [] = t"
@@ -105,6 +107,7 @@
lemma compose_assoc: "(a \<bullet> b) \<bullet> c =\<^sub>s a \<bullet> (b \<bullet> c)"
by auto
+
subsection {* Specification: Most general unifiers *}
definition
@@ -492,7 +495,6 @@
subsection {* Termination proof *}
-
termination unify
proof
let ?R = "measures [\<lambda>(M,N). card (vars_of M \<union> vars_of N),
@@ -532,23 +534,4 @@
qed
qed
-
-(*<*)end(*>*)
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+end