# HG changeset patch
# User haftmann
# Date 1205565076 -3600
# Node ID 014d93dc21996407c105a705f75c02870c06e9cd
# Parent  2bdb61a28971a08769d00f683d094c3dd634abb0
(continued)

diff -r 2bdb61a28971 -r 014d93dc2199 src/HOL/ex/Quickcheck.thy
--- a/src/HOL/ex/Quickcheck.thy	Sat Mar 15 08:11:15 2008 +0100
+++ b/src/HOL/ex/Quickcheck.thy	Sat Mar 15 08:11:16 2008 +0100
@@ -282,6 +282,10 @@
 
 subsection {* Examples *}
 
+ML {* Quickcheck.mk_generator_expr
+  @{term "\<lambda>(n::nat) (m::nat) (q::nat). n = m + q + 1"} [@{typ nat}, @{typ nat}, @{typ nat}]
+|> Sign.string_of_term @{theory} *}
+
 (*setup {* Quickcheck.VALUE @{term "\<lambda>(n::nat) (m::nat) (q::nat). n = m + q + 1"} [@{typ nat}, @{typ nat}, @{typ nat}] *}
 export_code VALUE in SML module_name QuickcheckExample file "~~/../../gen_code/quickcheck.ML"
 use "~~/../../gen_code/quickcheck.ML"
@@ -387,11 +391,4 @@
 ML {* f 8 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 ML {* f 8 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
 
-definition "map2 f xs ys = map (split f) (zip xs ys)"
-
-lemma
-  assumes "\<And>x. f x x = x"
-  shows "map2 f xs xs = xs"
-  by (induct xs) (simp_all add: map2_def assms)
-
 end