diff -r c78f1d924bfe -r 3572bc633d9a src/HOL/ex/Codegenerator_Rat.thy --- 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