# 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