src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy
changeset 61424 c3658c18b7bc
parent 61145 497eb43a3064
child 63167 0909deb8059b
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -338,7 +338,7 @@
     1.4    "jad = apsnd transpose o length_permutate o map sparsify"
     1.5  
     1.6  definition
     1.7 -  "jad_mv v = inflate o split zip o apsnd (map listsum o transpose o map (map (\<lambda> (i, x). v ! i * x)))"
     1.8 +  "jad_mv v = inflate o case_prod zip o apsnd (map listsum o transpose o map (map (\<lambda> (i, x). v ! i * x)))"
     1.9  
    1.10  lemma "matrix (M::int list list) rs cs \<Longrightarrow> False"
    1.11  quickcheck[tester = smart_exhaustive, size = 6]