equal
deleted
inserted
replaced
127 |
127 |
128 instance .. |
128 instance .. |
129 |
129 |
130 end |
130 end |
131 |
131 |
132 code_thms implies |
|
133 declare simp_thms(17,19)[code del] |
|
134 code_thms implies |
|
135 |
|
136 subsubsection {* Invalid Lemma due to typo in lbal *} |
132 subsubsection {* Invalid Lemma due to typo in lbal *} |
137 |
133 |
138 lemma is_ord_l_bal: |
134 lemma is_ord_l_bal: |
139 "\<lbrakk> is_ord(MKT (x :: nat) l r h); height l = height r + 2 \<rbrakk> \<Longrightarrow> is_ord(l_bal(x,l,r))" |
135 "\<lbrakk> is_ord(MKT (x :: nat) l r h); height l = height r + 2 \<rbrakk> \<Longrightarrow> is_ord(l_bal(x,l,r))" |
140 quickcheck[tester = lazy_exhaustive, finite_types = false, default_type = nat, size = 1, timeout = 80, expect = counterexample] |
136 quickcheck[tester = lazy_exhaustive, finite_types = false, default_type = nat, size = 1, timeout = 80, expect = counterexample] |