--- a/src/HOL/SMT_Examples/SMT_Tests.thy Tue Jun 03 10:35:51 2014 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy Tue Jun 03 11:43:07 2014 +0200
@@ -184,7 +184,7 @@
by smt2+
-section {* Guidance for quantifier heuristics: patterns and weights *}
+section {* Guidance for quantifier heuristics: patterns *}
lemma
assumes "\<forall>x. SMT2.trigger [[SMT2.pat (f x)]] (f x = x)"
@@ -216,18 +216,6 @@
shows "R t"
using assms by smt2
-lemma
- assumes "ALL x. SMT2.trigger [[SMT2.pat (P x)]] (SMT2.weight 2 (P x --> Q x))"
- and "P t"
- shows "Q t"
- using assms by smt2
-
-lemma
- assumes "ALL x. SMT2.weight 1 (P x --> Q x)"
- and "P t"
- shows "Q t"
- using assms by smt2
-
section {* Meta-logical connectives *}