ex/Quickcheck_Examples.thy: respect distinction between sets and functions
authorhuffman
Sat, 13 Aug 2011 07:39:35 -0700
changeset 44189 4a80017c733f
parent 44179 9411ed32f3a7
child 44190 fe5504984937
ex/Quickcheck_Examples.thy: respect distinction between sets and functions
src/HOL/ex/Quickcheck_Examples.thy
--- a/src/HOL/ex/Quickcheck_Examples.thy	Sat Aug 13 12:23:51 2011 +0200
+++ b/src/HOL/ex/Quickcheck_Examples.thy	Sat Aug 13 07:39:35 2011 -0700
@@ -234,7 +234,7 @@
 oops
 
 lemma
-  "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-List.transpose xs. {..<i} (length ys)]"
+  "[| 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