# 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: