src/HOL/ex/Cartouche_Examples.thy

--- a/src/HOL/ex/Cartouche_Examples.thy	Wed Apr 09 17:54:09 2014 +0200
+++ b/src/HOL/ex/Cartouche_Examples.thy	Wed Apr 09 20:58:32 2014 +0200
@@ -27,6 +27,9 @@
   txt \<open>Of course, this can be nested inside formal comments and
     antiquotations, e.g. like this @{thm \<open>x = y\<close>} or this @{thm sym
     [OF \<open>x = y\<close>]}.\<close>
+
+  have "x = y"
+    by (tactic \<open>rtac @{thm \<open>x = y\<close>} 1\<close>)  -- \<open>more cartouches involving ML\<close>
 end