src/HOL/SMT.thy
changeset 41762 00060198de12
parent 41601 fda8511006f9
child 43230 dabf6e311213
     1.1 --- a/src/HOL/SMT.thy	Mon Feb 14 10:40:43 2011 +0100
     1.2 +++ b/src/HOL/SMT.thy	Mon Feb 14 12:25:26 2011 +0100
     1.3 @@ -247,6 +247,13 @@
     1.4  
     1.5  declare [[ smt_monomorph_limit = 10 ]]
     1.6  
     1.7 +text {*
     1.8 +In addition, the number of generated monomorphic instances is limited
     1.9 +by the following option.
    1.10 +*}
    1.11 +
    1.12 +declare [[ smt_monomorph_instances = 500 ]]
    1.13 +
    1.14  
    1.15  
    1.16  subsection {* Certificates *}