# HG changeset patch
# User haftmann
# Date 1233686250 -3600
# Node ID c78806b621e12e72ca9a2d92578f449a2bcd1519
# Parent  32d00a2a6f28063cfe3efdcb0bce08f280a42dc2# Parent  c566b63ce76a5ef09f540bd5ecc5ca2f1c2238c4
merged

diff -r 32d00a2a6f28 -r c78806b621e1 src/HOL/IsaMakefile
--- 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
diff -r 32d00a2a6f28 -r c78806b621e1 src/HOL/Reflection/ROOT.ML
--- /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