# HG changeset patch # User bulwahn # Date 1299836260 -3600 # Node ID 709c04e7b70332a9045dd59adcfc7c6e80a3fdf1 # Parent 383bbdad1650779f8717c9c1fd68b13cecd8cc84 adding serial instance of finite_4 in lazysmallcheck; changing code equations for implies diff -r 383bbdad1650 -r 709c04e7b703 src/HOL/Library/LSC.thy --- a/src/HOL/Library/LSC.thy Fri Mar 11 10:37:38 2011 +0100 +++ b/src/HOL/Library/LSC.thy Fri Mar 11 10:37:40 2011 +0100 @@ -289,6 +289,17 @@ end +instantiation Enum.finite_4 :: serial +begin + +definition series_finite_4 :: "Enum.finite_4 series" +where + "series_finite_4 = sum (cons Enum.finite_4.a\<^isub>1) (sum (cons Enum.finite_4.a\<^isub>2) (sum (cons Enum.finite_4.a\<^isub>3) (cons Enum.finite_4.a\<^isub>4)))" + +instance .. + +end + subsubsection {* class is_testable *} text {* The class is_testable ensures that all necessary type instances are generated. *} @@ -303,6 +314,8 @@ where "ensure_testable f = f" +declare simp_thms(17,19)[code del] + subsubsection {* Setting up the counterexample generator *} use "~~/src/HOL/Tools/LSC/lazysmallcheck.ML" diff -r 383bbdad1650 -r 709c04e7b703 src/HOL/ex/LSC_Examples.thy --- a/src/HOL/ex/LSC_Examples.thy Fri Mar 11 10:37:38 2011 +0100 +++ b/src/HOL/ex/LSC_Examples.thy Fri Mar 11 10:37:40 2011 +0100 @@ -129,10 +129,6 @@ end -code_thms implies -declare simp_thms(17,19)[code del] -code_thms implies - subsubsection {* Invalid Lemma due to typo in lbal *} lemma is_ord_l_bal: