--- a/src/HOL/IsaMakefile Tue Feb 03 19:37:16 2009 +0100
+++ b/src/HOL/IsaMakefile Tue Feb 03 19:37:30 2009 +0100
@@ -835,7 +835,6 @@
ex/document/root.tex ex/Meson_Test.thy ex/set.thy \
ex/svc_funcs.ML ex/svc_test.thy \
ex/ImperativeQuicksort.thy \
- ex/BigO_Complex.thy \
ex/Arithmetic_Series_Complex.thy ex/HarmonicSeries.thy \
ex/Sqrt.thy ex/Sqrt_Script.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Reflection/ROOT.ML Tue Feb 03 19:37:30 2009 +0100
@@ -0,0 +1,2 @@
+
+use_thys ["Cooper", "Ferrack", "MIR"];
\ No newline at end of file