# HG changeset patch
# User huffman
# Date 1273728790 25200
# Node ID c6bae4456741758122c0bf2e2c85fb57167324da
# Parent  a20c5484dc9c26c560aecf2bf642dc7edbbad035
use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document

diff -r a20c5484dc9c -r c6bae4456741 src/HOL/Lazy_Sequence.thy
--- a/src/HOL/Lazy_Sequence.thy	Thu May 13 00:44:48 2010 +0200
+++ b/src/HOL/Lazy_Sequence.thy	Wed May 12 22:33:10 2010 -0700
@@ -136,7 +136,7 @@
   datatypes lazy_sequence = Lazy_Sequence
   functions map yield yieldn
 
-section {* With Hit Bound Value *}
+subsection {* With Hit Bound Value *}
 text {* assuming in negative context *}
 
 types 'a hit_bound_lazy_sequence = "'a option lazy_sequence"
diff -r a20c5484dc9c -r c6bae4456741 src/HOL/New_DSequence.thy
--- a/src/HOL/New_DSequence.thy	Thu May 13 00:44:48 2010 +0200
+++ b/src/HOL/New_DSequence.thy	Wed May 12 22:33:10 2010 -0700
@@ -7,7 +7,7 @@
 imports Random_Sequence
 begin
 
-section {* Positive Depth-Limited Sequence *}
+subsection {* Positive Depth-Limited Sequence *}
 
 types 'a pos_dseq = "code_numeral => 'a Lazy_Sequence.lazy_sequence"
 
@@ -43,7 +43,7 @@
 where
   "pos_map f xq = (%i. Lazy_Sequence.map f (xq i))"
 
-section {* Negative Depth-Limited Sequence *}
+subsection {* Negative Depth-Limited Sequence *}
 
 types 'a neg_dseq = "code_numeral => 'a Lazy_Sequence.hit_bound_lazy_sequence"
 
@@ -79,7 +79,7 @@
 where
   "neg_map f xq = (%i. Lazy_Sequence.hb_map f (xq i))"
 
-section {* Negation *}
+subsection {* Negation *}
 
 definition pos_not_seq :: "unit neg_dseq => unit pos_dseq"
 where
diff -r a20c5484dc9c -r c6bae4456741 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Thu May 13 00:44:48 2010 +0200
+++ b/src/HOL/SMT.thy	Wed May 12 22:33:10 2010 -0700
@@ -26,7 +26,7 @@
 
 
 
-section {* Triggers for quantifier instantiation *}
+subsection {* Triggers for quantifier instantiation *}
 
 text {*
 Some SMT solvers support triggers for quantifier instantiation.
@@ -53,7 +53,7 @@
 
 
 
-section {* Higher-order encoding *}
+subsection {* Higher-order encoding *}
 
 text {*
 Application is made explicit for constants occurring with varying
@@ -74,7 +74,7 @@
 
 
 
-section {* First-order logic *}
+subsection {* First-order logic *}
 
 text {*
 Some SMT solvers require a strict separation between formulas and
@@ -91,7 +91,7 @@
 
 
 
-section {* Setup *}
+subsection {* Setup *}
 
 use "Tools/SMT/smt_monomorph.ML"
 use "Tools/SMT/smt_normalize.ML"
@@ -118,7 +118,7 @@
 
 
 
-section {* Configuration *}
+subsection {* Configuration *}
 
 text {*
 The current configuration can be printed by the command
@@ -224,7 +224,7 @@
 
 
 
-section {* Schematic rules for Z3 proof reconstruction *}
+subsection {* Schematic rules for Z3 proof reconstruction *}
 
 text {*
 Several prof rules of Z3 are not very well documented.  There are two