--- a/src/HOL/IsaMakefile Wed Jul 21 18:11:51 2010 +0200
+++ b/src/HOL/IsaMakefile Wed Jul 21 18:11:51 2010 +0200
@@ -424,7 +424,8 @@
Library/Poly_Deriv.thy Library/Polynomial.thy \
Library/Predicate_Compile_Quickcheck.thy Library/Preorder.thy \
Library/Product_Vector.thy Library/Product_ord.thy \
- Library/Product_plus.thy Library/Quicksort.thy \
+ Library/Product_plus.thy Library/Quickcheck_Types.thy \
+ Library/Quicksort.thy \
Library/Quotient_List.thy Library/Quotient_Option.thy \
Library/Quotient_Product.thy Library/Quotient_Sum.thy \
Library/Quotient_Syntax.thy Library/Quotient_Type.thy \
@@ -990,7 +991,8 @@
ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy \
ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy \
ex/Multiquote.thy ex/NatSum.thy ex/Numeral.thy ex/PER.thy \
- ex/PresburgerEx.thy ex/Primrec.thy ex/Quickcheck_Examples.thy \
+ ex/PresburgerEx.thy ex/Primrec.thy \
+ ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy \
ex/ROOT.ML ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy \
ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \
ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Sudoku.thy \
--- a/src/HOL/ex/ROOT.ML Wed Jul 21 18:11:51 2010 +0200
+++ b/src/HOL/ex/ROOT.ML Wed Jul 21 18:11:51 2010 +0200
@@ -59,6 +59,7 @@
"HarmonicSeries",
"Refute_Examples",
"Quickcheck_Examples",
+ "Quickcheck_Lattice_Examples",
"Landau",
"Execute_Choice",
"Summation",