--- a/src/HOL/SMT.thy Mon Nov 22 15:45:43 2010 +0100
+++ b/src/HOL/SMT.thy Mon Nov 22 23:37:00 2010 +0100
@@ -54,6 +54,33 @@
+subsection {* Quantifier weights *}
+
+text {*
+Weight annotations to quantifiers influence the priority of quantifier
+instantiations. They should be handled with care for solvers, which support
+them, because incorrect choices of weights might render a problem unsolvable.
+*}
+
+definition weight :: "int \<Rightarrow> bool \<Rightarrow> bool" where "weight _ P = P"
+
+text {*
+Weights must be non-negative. The value @{text 0} is equivalent to providing
+no weight at all.
+
+Weights should only be used at quantifiers and only inside triggers (if the
+quantifier has triggers). Valid usages of weights are as follows:
+
+\begin{itemize}
+\item
+@{term "\<forall>x. trigger [[pat (P x)]] (weight 2 (P x))"}
+\item
+@{term "\<forall>x. weight 3 (P x)"}
+\end{itemize}
+*}
+
+
+
subsection {* Distinctness *}
text {*
@@ -342,7 +369,7 @@
hide_type (open) pattern
hide_const Pattern term_eq
-hide_const (open) trigger pat nopat distinct fun_app z3div z3mod
+hide_const (open) trigger pat nopat weight distinct fun_app z3div z3mod