src/HOL/Library/LSC.thy
changeset 41910 709c04e7b703
parent 41909 383bbdad1650
child 41912 1848775589e5
--- 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"