# HG changeset patch
# User wenzelm
# Date 1228945602 -3600
# Node ID d5a5888b8c54288d87e8c00f97eb030aca253a96
# Parent  9dbf8249d979a67aac1e79a481b3819323264057
requires RComplete;

diff -r 9dbf8249d979 -r d5a5888b8c54 src/HOL/ex/MIR.thy
--- a/src/HOL/ex/MIR.thy	Wed Dec 10 06:34:10 2008 -0800
+++ b/src/HOL/ex/MIR.thy	Wed Dec 10 22:46:42 2008 +0100
@@ -1,9 +1,9 @@
-(*  Title:      Complex/ex/MIR.thy
+(*  Title:      HOL/ex/MIR.thy
     Author:     Amine Chaieb
 *)
 
 theory MIR
-imports List Real Code_Integer Efficient_Nat
+imports Main RComplete Code_Integer Efficient_Nat
 uses ("mirtac.ML")
 begin