author | haftmann |
Thu, 13 Apr 2017 10:10:08 +0200 (2017-04-13) | |
changeset 65481 | b11b7ad22684 |
parent 65480 | 5407bc278c9a |
child 65482 | 721feefce9c6 |
--- 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)])"