# 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 "\(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 "\(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 "\x. f x x = x" - shows "map2 f xs xs = xs" - by (induct xs) (simp_all add: map2_def assms) - end