# HG changeset patch # User bulwahn # Date 1329927935 -3600 # Node ID 0a28a5a97d718170d55b89bf301319682021e92e # Parent 6893119867781d5550a25b33f6fa7ae91b89a417 adding some examples with find_unused_assms command diff -r 689311986778 -r 0a28a5a97d71 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Feb 22 17:22:53 2012 +0100 +++ b/src/HOL/IsaMakefile Wed Feb 22 17:25:35 2012 +0100 @@ -1513,6 +1513,7 @@ HOL-Quickcheck_Examples: HOL $(LOG)/HOL-Quickcheck_Examples.gz $(LOG)/HOL-Quickcheck_Examples.gz: $(OUT)/HOL \ + Quickcheck_Examples/Find_Unused_Assms.thy \ Quickcheck_Examples/Quickcheck_Examples.thy \ Quickcheck_Examples/Quickcheck_Lattice_Examples.thy \ Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy diff -r 689311986778 -r 0a28a5a97d71 src/HOL/Quickcheck_Examples/Find_Unused_Assms_Examples.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Quickcheck_Examples/Find_Unused_Assms_Examples.thy Wed Feb 22 17:25:35 2012 +0100 @@ -0,0 +1,27 @@ +theory Find_Unused_Assms_Examples +imports Main +begin + +section {* Arithmetics *} + +declare [[quickcheck_finite_types = false]] + +find_unused_assms Divides +find_unused_assms GCD +find_unused_assms MacLaurin + +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 \ No newline at end of file diff -r 689311986778 -r 0a28a5a97d71 src/HOL/Quickcheck_Examples/ROOT.ML --- a/src/HOL/Quickcheck_Examples/ROOT.ML Wed Feb 22 17:22:53 2012 +0100 +++ b/src/HOL/Quickcheck_Examples/ROOT.ML Wed Feb 22 17:25:35 2012 +0100 @@ -1,4 +1,5 @@ use_thys [ + "Find_Unused_Assms", "Quickcheck_Examples", "Quickcheck_Lattice_Examples" ];