reactivated Find_Unused_Assms_Examples to avoid untested / dead stuff in the repository;
moved the whole HOL-Quickcheck_Examples target from "all" to "full" for now -- it does not terminate in certain situations (to be investigated further);
1.1 --- a/src/HOL/IsaMakefile Mon Feb 27 11:53:08 2012 +0100
1.2 +++ b/src/HOL/IsaMakefile Mon Feb 27 12:12:28 2012 +0100
1.3 @@ -61,7 +61,6 @@
1.4 HOL-Nitpick_Examples \
1.5 HOL-Number_Theory \
1.6 HOL-Old_Number_Theory \
1.7 - HOL-Quickcheck_Examples \
1.8 HOL-Quotient_Examples \
1.9 HOL-Predicate_Compile_Examples \
1.10 HOL-Prolog \
1.11 @@ -96,7 +95,7 @@
1.12 HOL-Nominal-Examples
1.13
1.14 all: test-no-smlnj test images-no-smlnj images
1.15 -full: all benchmark
1.16 +full: all benchmark HOL-Quickcheck_Examples
1.17 smlnj: test images
1.18
1.19
2.1 --- a/src/HOL/Quickcheck_Examples/ROOT.ML Mon Feb 27 11:53:08 2012 +0100
2.2 +++ b/src/HOL/Quickcheck_Examples/ROOT.ML Mon Feb 27 12:12:28 2012 +0100
2.3 @@ -1,4 +1,5 @@
2.4 use_thys [
2.5 + "Find_Unused_Assms_Examples",
2.6 "Quickcheck_Examples",
2.7 "Quickcheck_Lattice_Examples"
2.8 ];