--- 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";