# HG changeset patch
# User bulwahn
# Date 1299836261 -3600
# Node ID c6e66b32ce165a14301695bb0bfc1f225dbe92b8
# Parent  709c04e7b70332a9045dd59adcfc7c6e80a3fdf1
adding lazysmallcheck example theory to HOL-ex session

diff -r 709c04e7b703 -r c6e66b32ce16 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Mar 11 10:37:40 2011 +0100
+++ b/src/HOL/IsaMakefile	Fri Mar 11 10:37:41 2011 +0100
@@ -1039,6 +1039,7 @@
   ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy		\
   ex/Interpretation_with_Defs.thy ex/Intuitionistic.thy ex/Lagrange.thy	\
   ex/List_to_Set_Comprehension_Examples.thy ex/LocaleTest2.thy		\
+  ex/LSC_Examples.thy \
   ex/MT.thy ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy	\
   ex/Multiquote.thy ex/NatSum.thy ex/Normalization_by_Evaluation.thy	\
   ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy		\
diff -r 709c04e7b703 -r c6e66b32ce16 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Fri Mar 11 10:37:40 2011 +0100
+++ b/src/HOL/ex/ROOT.ML	Fri Mar 11 10:37:41 2011 +0100
@@ -73,7 +73,8 @@
   "Quicksort",
   "Birthday_Paradoxon",
   "List_to_Set_Comprehension_Examples",
-  "Set_Algebras"
+  "Set_Algebras",
+  "LSC_Examples"
 ];
 
 use_thy "SVC_Oracle";