# HG changeset patch
# User wenzelm
# Date 1180905407 -7200
# Node ID 87ad6e8a5f2cd0cac4460fc51d4886372d215b8b
# Parent  01c4d19f597ebc56d7f079bfff2bce47c2205e76
tuned document;

diff -r 01c4d19f597e -r 87ad6e8a5f2c src/HOL/ex/CTL.thy
--- 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
diff -r 01c4d19f597e -r 87ad6e8a5f2c src/HOL/ex/LocaleTest2.thy
--- 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 *}
 
diff -r 01c4d19f597e -r 87ad6e8a5f2c src/HOL/ex/Refute_Examples.thy
--- 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: *}
 
diff -r 01c4d19f597e -r 87ad6e8a5f2c src/HOL/ex/Sudoku.thy
--- 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 {*
diff -r 01c4d19f597e -r 87ad6e8a5f2c src/HOL/ex/ThreeDivides.thy
--- 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
diff -r 01c4d19f597e -r 87ad6e8a5f2c src/HOL/ex/Unification.thy
--- 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