# HG changeset patch
# User bulwahn
# Date 1301504996 -7200
# Node ID 32c3bb5e1b1af2a32cb794104255c69672494404
# Parent  efd229daeb2c6c45e7e7c3f95cc6dd90de58f88a
removing junk that should not have been committed

diff -r efd229daeb2c -r 32c3bb5e1b1a src/HOL/Quickcheck.thy
--- a/src/HOL/Quickcheck.thy	Wed Mar 30 17:54:10 2011 +0200
+++ b/src/HOL/Quickcheck.thy	Wed Mar 30 19:09:56 2011 +0200
@@ -209,12 +209,5 @@
 hide_type (open) randompred
 hide_const (open) random collapse beyond random_fun_aux random_fun_lift
   iter' iter empty single bind union if_randompred iterate_upto not_randompred Random map
-declare [[quickcheck_timing]]
-lemma
-  "rev xs = xs"
-quickcheck[tester = random, finite_types = true, report = false]
-
-quickcheck[tester = random, finite_types = false, report = false]
-oops
 
 end