requires RComplete;
authorwenzelm
Wed, 10 Dec 2008 22:46:42 +0100
changeset 29042 d5a5888b8c54
parent 29041 9dbf8249d979
child 29043 409d1ca929b5
requires RComplete;
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