ex/Quickcheck_Examples.thy: respect distinction between sets and functions
authorhuffman
Sat Aug 13 07:39:35 2011 -0700 (2011-08-13)
changeset 441894a80017c733f
parent 44179 9411ed32f3a7
child 44190 fe5504984937
ex/Quickcheck_Examples.thy: respect distinction between sets and functions
src/HOL/ex/Quickcheck_Examples.thy
     1.1 --- a/src/HOL/ex/Quickcheck_Examples.thy	Sat Aug 13 12:23:51 2011 +0200
     1.2 +++ b/src/HOL/ex/Quickcheck_Examples.thy	Sat Aug 13 07:39:35 2011 -0700
     1.3 @@ -234,7 +234,7 @@
     1.4  oops
     1.5  
     1.6  lemma
     1.7 -  "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-List.transpose xs. {..<i} (length ys)]"
     1.8 +  "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-List.transpose xs. length ys \<in> {..<i}]"
     1.9  quickcheck[random]
    1.10  quickcheck[exhaustive, expect = counterexample]
    1.11  oops