# HG changeset patch
# User bulwahn
# Date 1279728711 -7200
# Node ID 67ccea8a47616cf73d3202779b287b0473ef22d2
# Parent  cb55fd65faa6ca886fd67903cd3d0d6babe2d989
added new theories to IsaMakefile and ROOT.ML

diff -r cb55fd65faa6 -r 67ccea8a4761 src/HOL/IsaMakefile
--- 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		\
diff -r cb55fd65faa6 -r 67ccea8a4761 src/HOL/ex/ROOT.ML
--- 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",