use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
authorhuffman
Wed May 12 22:33:10 2010 -0700 (2010-05-12)
changeset 36902c6bae4456741
parent 36901 a20c5484dc9c
child 36903 489c1fbbb028
child 36904 3e200347a22e
use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
src/HOL/Lazy_Sequence.thy
src/HOL/New_DSequence.thy
src/HOL/SMT.thy
     1.1 --- a/src/HOL/Lazy_Sequence.thy	Thu May 13 00:44:48 2010 +0200
     1.2 +++ b/src/HOL/Lazy_Sequence.thy	Wed May 12 22:33:10 2010 -0700
     1.3 @@ -136,7 +136,7 @@
     1.4    datatypes lazy_sequence = Lazy_Sequence
     1.5    functions map yield yieldn
     1.6  
     1.7 -section {* With Hit Bound Value *}
     1.8 +subsection {* With Hit Bound Value *}
     1.9  text {* assuming in negative context *}
    1.10  
    1.11  types 'a hit_bound_lazy_sequence = "'a option lazy_sequence"
     2.1 --- a/src/HOL/New_DSequence.thy	Thu May 13 00:44:48 2010 +0200
     2.2 +++ b/src/HOL/New_DSequence.thy	Wed May 12 22:33:10 2010 -0700
     2.3 @@ -7,7 +7,7 @@
     2.4  imports Random_Sequence
     2.5  begin
     2.6  
     2.7 -section {* Positive Depth-Limited Sequence *}
     2.8 +subsection {* Positive Depth-Limited Sequence *}
     2.9  
    2.10  types 'a pos_dseq = "code_numeral => 'a Lazy_Sequence.lazy_sequence"
    2.11  
    2.12 @@ -43,7 +43,7 @@
    2.13  where
    2.14    "pos_map f xq = (%i. Lazy_Sequence.map f (xq i))"
    2.15  
    2.16 -section {* Negative Depth-Limited Sequence *}
    2.17 +subsection {* Negative Depth-Limited Sequence *}
    2.18  
    2.19  types 'a neg_dseq = "code_numeral => 'a Lazy_Sequence.hit_bound_lazy_sequence"
    2.20  
    2.21 @@ -79,7 +79,7 @@
    2.22  where
    2.23    "neg_map f xq = (%i. Lazy_Sequence.hb_map f (xq i))"
    2.24  
    2.25 -section {* Negation *}
    2.26 +subsection {* Negation *}
    2.27  
    2.28  definition pos_not_seq :: "unit neg_dseq => unit pos_dseq"
    2.29  where
     3.1 --- a/src/HOL/SMT.thy	Thu May 13 00:44:48 2010 +0200
     3.2 +++ b/src/HOL/SMT.thy	Wed May 12 22:33:10 2010 -0700
     3.3 @@ -26,7 +26,7 @@
     3.4  
     3.5  
     3.6  
     3.7 -section {* Triggers for quantifier instantiation *}
     3.8 +subsection {* Triggers for quantifier instantiation *}
     3.9  
    3.10  text {*
    3.11  Some SMT solvers support triggers for quantifier instantiation.
    3.12 @@ -53,7 +53,7 @@
    3.13  
    3.14  
    3.15  
    3.16 -section {* Higher-order encoding *}
    3.17 +subsection {* Higher-order encoding *}
    3.18  
    3.19  text {*
    3.20  Application is made explicit for constants occurring with varying
    3.21 @@ -74,7 +74,7 @@
    3.22  
    3.23  
    3.24  
    3.25 -section {* First-order logic *}
    3.26 +subsection {* First-order logic *}
    3.27  
    3.28  text {*
    3.29  Some SMT solvers require a strict separation between formulas and
    3.30 @@ -91,7 +91,7 @@
    3.31  
    3.32  
    3.33  
    3.34 -section {* Setup *}
    3.35 +subsection {* Setup *}
    3.36  
    3.37  use "Tools/SMT/smt_monomorph.ML"
    3.38  use "Tools/SMT/smt_normalize.ML"
    3.39 @@ -118,7 +118,7 @@
    3.40  
    3.41  
    3.42  
    3.43 -section {* Configuration *}
    3.44 +subsection {* Configuration *}
    3.45  
    3.46  text {*
    3.47  The current configuration can be printed by the command
    3.48 @@ -224,7 +224,7 @@
    3.49  
    3.50  
    3.51  
    3.52 -section {* Schematic rules for Z3 proof reconstruction *}
    3.53 +subsection {* Schematic rules for Z3 proof reconstruction *}
    3.54  
    3.55  text {*
    3.56  Several prof rules of Z3 are not very well documented.  There are two