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