# HG changeset patch
# User wenzelm
# Date 1554979102 -7200
# Node ID 62b875ba33e179bf42af125d8245f301f5ba6fbe
# Parent  5ae2f266885fbba9773121c3eade8aa712ddaf6f
prefer local options;

diff -r 5ae2f266885f -r 62b875ba33e1 src/Benchmarks/Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy
--- a/src/Benchmarks/Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy	Thu Apr 11 12:18:03 2019 +0200
+++ b/src/Benchmarks/Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy	Thu Apr 11 12:38:22 2019 +0200
@@ -4,24 +4,31 @@
 
 section \<open>Arithmetics\<close>
 
-declare [[quickcheck_finite_types = false]]
+context notes [[quickcheck_finite_types = false]]
+begin
+  find_unused_assms Divides
+  find_unused_assms GCD
+  find_unused_assms Real
+end
 
-find_unused_assms Divides
-find_unused_assms GCD
-find_unused_assms Real
 
 section \<open>Set Theory\<close>
 
-declare [[quickcheck_finite_types = true]]
+context notes [[quickcheck_finite_types = true]]
+begin
+  find_unused_assms Fun
+  find_unused_assms Relation
+  find_unused_assms Set
+  find_unused_assms Wellfounded
+end
 
-find_unused_assms Fun
-find_unused_assms Relation
-find_unused_assms Set
-find_unused_assms Wellfounded
 
 section \<open>Datatypes\<close>
 
-find_unused_assms List
-find_unused_assms Map
+context notes [[quickcheck_finite_types = true]]
+begin
+  find_unused_assms List
+  find_unused_assms Map
+end
 
 end