src/HOL/ex/LSC_Examples.thy
changeset 41913 34360908cb78
parent 41912 1848775589e5
equal deleted inserted replaced
41912:1848775589e5 41913:34360908cb78
   132 
   132 
   133 subsubsection {* Invalid Lemma due to typo in lbal *}
   133 subsubsection {* Invalid Lemma due to typo in lbal *}
   134 
   134 
   135 lemma is_ord_l_bal:
   135 lemma is_ord_l_bal:
   136  "\<lbrakk> is_ord(MKT (x :: nat) l r h); height l = height r + 2 \<rbrakk> \<Longrightarrow> is_ord(l_bal(x,l,r))"
   136  "\<lbrakk> is_ord(MKT (x :: nat) l r h); height l = height r + 2 \<rbrakk> \<Longrightarrow> is_ord(l_bal(x,l,r))"
   137 quickcheck[tester = lazy_exhaustive, finite_types = false, default_type = nat, size = 1, timeout = 80, expect = counterexample]
   137 quickcheck[tester = lazy_exhaustive, finite_types = false, default_type = nat, size = 1, timeout = 100, expect = counterexample]
   138 oops
   138 oops
   139 
   139 
   140 
   140 
   141 end
   141 end