# HG changeset patch
# User bulwahn
# Date 1343126219 -7200
# Node ID 1959baa226321b1342bd803ad1931eb02cb7742d
# Parent  aff95a0212d8e33c02b4147c3fc1cf28757fd127
moving a first Quickcheck example with many computations into a separate session Quickcheck_Benchmark

diff -r aff95a0212d8 -r 1959baa22632 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Jul 24 08:12:15 2012 +0200
+++ b/src/HOL/IsaMakefile	Tue Jul 24 12:36:59 2012 +0200
@@ -82,6 +82,7 @@
 
 benchmark: \
   HOL-Datatype_Benchmark \
+  HOL-Quickcheck_Benchmark \
   HOL-Record_Benchmark
 
 images-no-smlnj: \
@@ -1509,8 +1510,8 @@
 HOL-Quickcheck_Examples: HOL $(LOG)/HOL-Quickcheck_Examples.gz
 
 $(LOG)/HOL-Quickcheck_Examples.gz: $(OUT)/HOL				\
+  Quickcheck_Examples/ROOT.ML						\
   Quickcheck_Examples/Completeness.thy					\
-  Quickcheck_Examples/Find_Unused_Assms_Examples.thy			\
   Quickcheck_Examples/Hotel_Example.thy					\
   Quickcheck_Examples/Needham_Schroeder_Base.thy			\
   Quickcheck_Examples/Needham_Schroeder_No_Attacker_Example.thy		\
@@ -1816,6 +1817,15 @@
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Record_Benchmark
 
 
+## HOL-Quickcheck_Benchmark
+
+HOL-Quickcheck_Benchmark: HOL $(LOG)/HOL-Quickcheck_Benchmark.gz
+
+$(LOG)/HOL-Quickcheck_Benchmark.gz: $(OUT)/HOL				\
+  Quickcheck_Benchmark/ROOT.ML						\
+  Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy
+	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Quickcheck_Benchmark
+
 
 ## clean
 
diff -r aff95a0212d8 -r 1959baa22632 src/HOL/Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy	Tue Jul 24 12:36:59 2012 +0200
@@ -0,0 +1,28 @@
+theory Find_Unused_Assms_Examples
+imports Complex_Main
+begin
+
+section {* Arithmetics *}
+
+declare [[quickcheck_finite_types = false]]
+
+find_unused_assms Divides
+find_unused_assms GCD
+find_unused_assms RealDef
+find_unused_assms RComplete
+
+section {* Set Theory *}
+
+declare [[quickcheck_finite_types = true]]
+
+find_unused_assms Fun
+find_unused_assms Relation
+find_unused_assms Set
+find_unused_assms Wellfounded
+
+section {* Datatypes *}
+
+find_unused_assms List
+find_unused_assms Map
+
+end
diff -r aff95a0212d8 -r 1959baa22632 src/HOL/Quickcheck_Benchmark/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quickcheck_Benchmark/ROOT.ML	Tue Jul 24 12:36:59 2012 +0200
@@ -0,0 +1,1 @@
+use_thys ["Find_Unused_Assms_Examples"]
diff -r aff95a0212d8 -r 1959baa22632 src/HOL/Quickcheck_Examples/Find_Unused_Assms_Examples.thy
--- a/src/HOL/Quickcheck_Examples/Find_Unused_Assms_Examples.thy	Tue Jul 24 08:12:15 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-theory Find_Unused_Assms_Examples
-imports Complex_Main
-begin
-
-section {* Arithmetics *}
-
-declare [[quickcheck_finite_types = false]]
-
-find_unused_assms Divides
-find_unused_assms GCD
-find_unused_assms RealDef
-find_unused_assms RComplete
-
-section {* Set Theory *}
-
-declare [[quickcheck_finite_types = true]]
-
-find_unused_assms Fun
-find_unused_assms Relation
-find_unused_assms Set
-find_unused_assms Wellfounded
-
-section {* Datatypes *}
-
-find_unused_assms List
-find_unused_assms Map
-
-end