src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy

   | "mirror (Branch l r) = Branch (mirror r) (mirror l)"
 
 theorem "plant (rev (leaves xt)) = mirror xt"
   quickcheck[random, expect = counterexample]
   quickcheck[exhaustive, expect = counterexample]
-    \<comment>\<open>Wrong!\<close> 
+    \<comment> \<open>Wrong!\<close> 
   oops
 
 theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt"
   quickcheck[random, expect = counterexample]
   quickcheck[exhaustive, expect = counterexample]
-    \<comment>\<open>Wrong!\<close> 
+    \<comment> \<open>Wrong!\<close> 
   oops
 
 datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"
 
 primrec inOrder :: "'a ntree \<Rightarrow> 'a list" where

   | "root (Node f x y) = f"
 
 theorem "hd (inOrder xt) = root xt"
   quickcheck[random, expect = counterexample]
   quickcheck[exhaustive, expect = counterexample]
-  \<comment>\<open>Wrong!\<close> 
+  \<comment> \<open>Wrong!\<close> 
   oops
 
 
 subsection \<open>Exhaustive Testing beats Random Testing\<close>