Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy
changeset 67443 3abf6a722518
parent 67399 eab6ce8368fa
child 67613 ce654b0e6d69 
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Tue Jan 16 09:12:16 2018 +0100
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Tue Jan 16 09:30:00 2018 +0100
@@ -141,13 +141,13 @@
 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"
@@ -163,7 +163,7 @@
 theorem "hd (inOrder xt) = root xt"
   quickcheck[random, expect = counterexample]
   quickcheck[exhaustive, expect = counterexample]
-  \<comment>\<open>Wrong!\<close> 
+  \<comment> \<open>Wrong!\<close> 
   oops
isabelle