src/HOL/Datatype_Examples/Compat.thy
changeset 58442 039b54d9b5c4
parent 58392 00f5b1efc741
child 58889 5b7a9633cfa8
--- a/src/HOL/Datatype_Examples/Compat.thy	Thu Sep 25 13:30:57 2014 +0200
+++ b/src/HOL/Datatype_Examples/Compat.thy	Thu Sep 25 13:30:57 2014 +0200
@@ -40,10 +40,10 @@
 export_code old_len checking SML OCaml? Haskell? Scala
 
 lemma "Old_Nl = Old_Cns x xs"
-  nitpick [expect = genuine]
+  nitpick (* [expect = genuine] *)
   quickcheck [exhaustive, expect = counterexample]
   quickcheck [random, expect = counterexample]
-  quickcheck [narrowing, expect = counterexample]
+  quickcheck [narrowing (* , expect = counterexample *)]
   oops
 
 lemma "old_len xs = size xs"