adding lazysmallcheck example theory to HOL-ex session
authorbulwahn
Fri, 11 Mar 2011 10:37:41 +0100
changeset 41911 c6e66b32ce16
parent 41910 709c04e7b703
child 41912 1848775589e5
adding lazysmallcheck example theory to HOL-ex session
src/HOL/IsaMakefile
src/HOL/ex/ROOT.ML
--- 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		\
--- 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";