--- a/src/HOL/SMT_Examples/SMT_Tests.thy Mon Mar 26 10:42:06 2012 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy Mon Mar 26 11:01:04 2012 +0200
@@ -212,7 +212,7 @@
lemma
assumes "\<forall>x y. SMT.trigger [[SMT.pat (f x), SMT.pat (g y)]] (f x = g y)"
shows "f a = g b"
- using assms (* BROKEN by smt *) oops
+ using assms by smt
lemma
assumes "ALL x. SMT.trigger [[SMT.pat (P x)]] (P x --> Q x)"
@@ -853,7 +853,7 @@
using point.simps
using [[smt_datatypes, smt_oracle]]
using [[z3_options="AUTO_CONFIG=false"]]
- (* BROKEN by smt+ *) oops
+ by smt+
lemma
"cy (p \<lparr> cx := a \<rparr>) = cy p"
@@ -862,7 +862,7 @@
using point.simps
using [[smt_datatypes, smt_oracle]]
using [[z3_options="AUTO_CONFIG=false"]]
- (* BROKEN by smt+ *) oops
+ by smt+
lemma
"p1 = p2 \<longrightarrow> cx p1 = cx p2"
@@ -891,7 +891,7 @@
using point.simps bw_point.simps
using [[smt_datatypes, smt_oracle]]
using [[z3_options="AUTO_CONFIG=false"]]
- (* BROKEN by smt+ *) oops
+ by smt+
lemma
"\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> black := w \<rparr> = \<lparr> cx = 3, cy = 4, black = w \<rparr>"
@@ -905,7 +905,7 @@
using point.simps bw_point.simps
using [[smt_datatypes, smt_oracle]]
using [[z3_options="AUTO_CONFIG=false"]]
- (* BROKEN by smt *) oops
+ by smt
subsubsection {* Type definitions *}
@@ -919,7 +919,7 @@
using n1_def n2_def n3_def nplus_def
using [[smt_datatypes, smt_oracle]]
using [[z3_options="AUTO_CONFIG=false"]]
- (* BROKEN by smt+ *) oops
+ by smt+