src/HOL/SMT.thy
changeset 36902 c6bae4456741
parent 36899 bcd6fce5bf06
child 37124 fe22fc54b876
     1.1 --- a/src/HOL/SMT.thy	Thu May 13 00:44:48 2010 +0200
     1.2 +++ b/src/HOL/SMT.thy	Wed May 12 22:33:10 2010 -0700
     1.3 @@ -26,7 +26,7 @@
     1.4  
     1.5  
     1.6  
     1.7 -section {* Triggers for quantifier instantiation *}
     1.8 +subsection {* Triggers for quantifier instantiation *}
     1.9  
    1.10  text {*
    1.11  Some SMT solvers support triggers for quantifier instantiation.
    1.12 @@ -53,7 +53,7 @@
    1.13  
    1.14  
    1.15  
    1.16 -section {* Higher-order encoding *}
    1.17 +subsection {* Higher-order encoding *}
    1.18  
    1.19  text {*
    1.20  Application is made explicit for constants occurring with varying
    1.21 @@ -74,7 +74,7 @@
    1.22  
    1.23  
    1.24  
    1.25 -section {* First-order logic *}
    1.26 +subsection {* First-order logic *}
    1.27  
    1.28  text {*
    1.29  Some SMT solvers require a strict separation between formulas and
    1.30 @@ -91,7 +91,7 @@
    1.31  
    1.32  
    1.33  
    1.34 -section {* Setup *}
    1.35 +subsection {* Setup *}
    1.36  
    1.37  use "Tools/SMT/smt_monomorph.ML"
    1.38  use "Tools/SMT/smt_normalize.ML"
    1.39 @@ -118,7 +118,7 @@
    1.40  
    1.41  
    1.42  
    1.43 -section {* Configuration *}
    1.44 +subsection {* Configuration *}
    1.45  
    1.46  text {*
    1.47  The current configuration can be printed by the command
    1.48 @@ -224,7 +224,7 @@
    1.49  
    1.50  
    1.51  
    1.52 -section {* Schematic rules for Z3 proof reconstruction *}
    1.53 +subsection {* Schematic rules for Z3 proof reconstruction *}
    1.54  
    1.55  text {*
    1.56  Several prof rules of Z3 are not very well documented.  There are two