src/HOL/SMT.thy
changeset 43230 dabf6e311213
parent 41762 00060198de12
child 43927 3a87cb597832
     1.1 --- a/src/HOL/SMT.thy	Tue Jun 07 08:58:23 2011 +0200
     1.2 +++ b/src/HOL/SMT.thy	Tue Jun 07 10:24:16 2011 +0200
     1.3 @@ -245,14 +245,14 @@
     1.4  construction whose cycles are limited by the following option.
     1.5  *}
     1.6  
     1.7 -declare [[ smt_monomorph_limit = 10 ]]
     1.8 +declare [[ monomorph_max_rounds = 5 ]]
     1.9  
    1.10  text {*
    1.11  In addition, the number of generated monomorphic instances is limited
    1.12  by the following option.
    1.13  *}
    1.14  
    1.15 -declare [[ smt_monomorph_instances = 500 ]]
    1.16 +declare [[ monomorph_max_new_instances = 500 ]]
    1.17  
    1.18  
    1.19