src/HOL/SMT.thy

--- a/src/HOL/SMT.thy	Mon Feb 14 10:40:43 2011 +0100
+++ b/src/HOL/SMT.thy	Mon Feb 14 12:25:26 2011 +0100
@@ -247,6 +247,13 @@
 
 declare [[ smt_monomorph_limit = 10 ]]
 
+text {*
+In addition, the number of generated monomorphic instances is limited
+by the following option.
+*}
+
+declare [[ smt_monomorph_instances = 500 ]]
+
 
 
 subsection {* Certificates *}