src/HOL/SMT_Examples/SMT_Tests.thy

   "(\<forall>x y z. f x y = f z y \<longrightarrow> x = z) \<and> a \<noteq> d \<longrightarrow> f a b \<noteq> f d b"
   using [[smt2_oracle=true]] (* FIXME: disable refine_inj_axiom in Z3 *)
   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)"
   shows "f 1 = 1"
   using assms using [[smt2_trace]] by smt2

 lemma
   assumes "ALL x. SMT2.trigger [[SMT2.pat (P x)], [SMT2.pat (Q x)]]
     ((P x --> R x) & (Q x --> R x))"
   and "P t | Q t"
   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 *}