obsolete
authorhaftmann
Thu, 13 Apr 2017 10:10:08 +0200
changeset 65481 b11b7ad22684
parent 65480 5407bc278c9a
child 65482 721feefce9c6
obsolete
src/HOL/Quickcheck_Narrowing.thy
--- a/src/HOL/Quickcheck_Narrowing.thy	Thu Apr 13 10:10:06 2017 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy	Thu Apr 13 10:10:08 2017 +0200
@@ -84,10 +84,6 @@
 
 type_synonym 'a narrowing = "integer => 'a narrowing_cons"
 
-definition empty :: "'a narrowing"
-where
-  "empty d = Narrowing_cons (Narrowing_sum_of_products []) []"
-  
 definition cons :: "'a => 'a narrowing"
 where
   "cons a d = (Narrowing_cons (Narrowing_sum_of_products [[]]) [(\<lambda>_. a)])"