# HG changeset patch
# User blanchet
# Date 1399277023 -7200
# Node ID bc50d5e04e902add478c7fa5c25133ddb37807cb
# Parent  0c3d0bc98abee97627155faa82f4fd4dcbc63c7c
tuned comment

diff -r 0c3d0bc98abe -r bc50d5e04e90 src/HOL/SMT_Examples/SMT_Tests.thy
--- a/src/HOL/SMT_Examples/SMT_Tests.thy	Mon May 05 09:30:20 2014 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Mon May 05 10:03:43 2014 +0200
@@ -731,7 +731,7 @@
   "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow>
      p \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p"
   using point.simps bw_point.simps
-  by smt+ (* FIXME: bad Z3-4.3.x proof with smt2 *)
+  by smt+ (* smt2 FIXME: bad Z3 4.3.x proof *)
 
 lemma
   "\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> black := w \<rparr> = \<lparr> cx = 3, cy = 4, black = w \<rparr>"