src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy

--- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Sun Jun 03 19:06:56 2018 +0200
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Wed Jun 06 11:12:37 2018 +0200
@@ -186,7 +186,7 @@
 oops
 
 lemma
-  "i < length (List.transpose (List.transpose xs)) ==> xs ! i = map (%xs. xs ! i) (filter (\<lambda>ys. i < length ys) xs)"
+  "i < length (List.transpose (List.transpose xs)) ==> xs ! i = map (%xs. xs ! i) [ys<-xs. i < length ys]"
 quickcheck[random, iterations = 10000]
 quickcheck[exhaustive, expect = counterexample]
 oops
@@ -228,13 +228,13 @@
 oops
 
 lemma
-  "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) (filter (\<lambda>ys. i < length ys) (remdups xs))"
+  "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-remdups xs. i < length ys]"
 quickcheck[random]
 quickcheck[exhaustive, expect = counterexample]
 oops
 
 lemma
-  "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) (filter (\<lambda>ys. length ys \<in> {..<i}) (List.transpose xs))"
+  "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-List.transpose xs. length ys \<in> {..<i}]"
 quickcheck[random]
 quickcheck[exhaustive, expect = counterexample]
 oops