src/Benchmarks/Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy
author immler
Thu, 22 Feb 2018 15:17:25 +0100
changeset 67685 bdff8bf0a75b
parent 62290 658276428cfc
child 70118 62b875ba33e1
permissions -rw-r--r--
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations

theory Find_Unused_Assms_Examples
imports Complex_Main
begin

section \<open>Arithmetics\<close>

declare [[quickcheck_finite_types = false]]

find_unused_assms Divides
find_unused_assms GCD
find_unused_assms Real

section \<open>Set Theory\<close>

declare [[quickcheck_finite_types = true]]

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

end