# HG changeset patch
# User bulwahn
# Date 1299836256 -3600
# Node ID e163d435ccf7f9430b492719caa14ee0731a37d7
# Parent  e2611bc96022441bb4ab5db36f51f08852475998
adding Lazysmallcheck prototype to HOL-Library

diff -r e2611bc96022 -r e163d435ccf7 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Mar 11 10:37:35 2011 +0100
+++ b/src/HOL/IsaMakefile	Fri Mar 11 10:37:36 2011 +0100
@@ -469,6 +469,8 @@
   Library/While_Combinator.thy Library/Zorn.thy				\
   $(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML	\
   Library/reflection.ML Library/reify_data.ML				\
+  Library/LSC.thy $(SRC)/HOL/Tools/LSC/lazysmallcheck.ML 		\
+  $(SRC)/HOL/Tools/LSC/LazySmallCheck.hs 				\
   Library/document/root.bib Library/document/root.tex
 	@cd Library; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOL-Library