1.1 --- a/src/HOL/IsaMakefile	Wed Jul 21 18:11:51 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed Jul 21 18:11:51 2010 +0200
     1.3 @@ -424,7 +424,8 @@
     1.4    Library/Poly_Deriv.thy Library/Polynomial.thy				\
     1.5    Library/Predicate_Compile_Quickcheck.thy Library/Preorder.thy		\
     1.6    Library/Product_Vector.thy Library/Product_ord.thy			\
     1.7 -  Library/Product_plus.thy Library/Quicksort.thy			\
     1.8 +  Library/Product_plus.thy Library/Quickcheck_Types.thy 		\
     1.9 +  Library/Quicksort.thy 						\
    1.10    Library/Quotient_List.thy Library/Quotient_Option.thy			\
    1.11    Library/Quotient_Product.thy Library/Quotient_Sum.thy			\
    1.12    Library/Quotient_Syntax.thy Library/Quotient_Type.thy			\
    1.13 @@ -990,7 +991,8 @@
    1.14    ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy				\
    1.15    ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy			\
    1.16    ex/Multiquote.thy ex/NatSum.thy ex/Numeral.thy ex/PER.thy		\
    1.17 -  ex/PresburgerEx.thy ex/Primrec.thy ex/Quickcheck_Examples.thy		\
    1.18 +  ex/PresburgerEx.thy ex/Primrec.thy 					\
    1.19 +  ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy 	\
    1.20    ex/ROOT.ML ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy		\
    1.21    ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy		\
    1.22    ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Sudoku.thy		\

     2.1 --- a/src/HOL/ex/ROOT.ML	Wed Jul 21 18:11:51 2010 +0200
     2.2 +++ b/src/HOL/ex/ROOT.ML	Wed Jul 21 18:11:51 2010 +0200
     2.3 @@ -59,6 +59,7 @@
     2.4    "HarmonicSeries",
     2.5    "Refute_Examples",
     2.6    "Quickcheck_Examples",
     2.7 +  "Quickcheck_Lattice_Examples",
     2.8    "Landau",
     2.9    "Execute_Choice",
    2.10    "Summation",