src/HOL/ex/Quickcheck_Narrowing_Examples.thy
changeset 45658 c2c647a4c237
parent 45441 fb4ac1dd4fde
child 45773 7f2366dc8c0f
equal deleted inserted replaced
45657:862d68ee10f3 45658:c2c647a4c237
    96   quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
    96   quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
    97 oops
    97 oops
    98 
    98 
    99 lemma
    99 lemma
   100   "list_all2 P (rev xs) (rev ys) = list_all2 P xs (rev ys)"
   100   "list_all2 P (rev xs) (rev ys) = list_all2 P xs (rev ys)"
   101   quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
   101   quickcheck[tester = narrowing, finite_types = false, expect = counterexample, timeout = 60]
   102 oops
   102 oops
   103 
   103 
   104 lemma "map f xs = F f xs"
   104 lemma "map f xs = F f xs"
   105   quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
   105   quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
   106 oops
   106 oops