src/HOL/IsaMakefile
changeset 37917 67ccea8a4761
parent 37884 314a88278715
child 37921 1e846be00ddf
--- 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		\