| changeset 22507 | 3572bc633d9a |
| parent 22071 | ebcfe7c2499d |
| child 22803 | 5129e02f4df2 |
--- a/src/HOL/ex/Codegenerator_Rat.thy Fri Mar 23 09:40:49 2007 +0100 +++ b/src/HOL/ex/Codegenerator_Rat.thy Fri Mar 23 09:40:50 2007 +0100 @@ -6,7 +6,7 @@ header {* Simple example for executable rational numbers *} theory Codegenerator_Rat -imports ExecutableRat EfficientNat +imports EfficientNat ExecutableRat begin definition