author | haftmann |
Fri, 28 Mar 2008 22:01:04 +0100 | |
changeset 26469 | 6deb216d726f |
parent 26468 | bb6a015219cf |
child 26470 | e44d24620515 |
--- a/src/HOL/ex/Efficient_Nat_examples.thy Fri Mar 28 22:01:03 2008 +0100 +++ b/src/HOL/ex/Efficient_Nat_examples.thy Fri Mar 28 22:01:04 2008 +0100 @@ -6,7 +6,7 @@ header {* Simple examples for Efficient\_Nat theory. *} theory Efficient_Nat_examples -imports "~~/src/HOL/Real/RealDef" Efficient_Nat +imports Main "~~/src/HOL/Real/RealDef" Efficient_Nat begin fun