changeset 28523 | 5818d9cfb2e7 |
parent 26469 | 6deb216d726f |
child 28661 | a287d0e8aa9d |
--- a/src/HOL/ex/Efficient_Nat_examples.thy Tue Oct 07 16:07:33 2008 +0200 +++ b/src/HOL/ex/Efficient_Nat_examples.thy Tue Oct 07 16:07:40 2008 +0200 @@ -3,7 +3,7 @@ Author: Florian Haftmann, TU Muenchen *) -header {* Simple examples for Efficient\_Nat theory. *} +header {* Simple examples for Efficient\_Nat theory. *} theory Efficient_Nat_examples imports Main "~~/src/HOL/Real/RealDef" Efficient_Nat