| changeset 29629 | 5111ce425e7a |
| parent 26086 | 3c243098b64a |
| child 29640 | 741f26190c96 |
--- a/src/HOL/Word/Examples/WordExamples.thy Mon Jan 26 22:14:16 2009 +0100 +++ b/src/HOL/Word/Examples/WordExamples.thy Mon Jan 26 22:14:17 2009 +0100 @@ -1,5 +1,4 @@ (* - ID: $Id$ Author: Gerwin Klein, NICTA Examples demonstrating and testing various word operations. @@ -7,7 +6,8 @@ header "Examples of word operations" -theory WordExamples imports WordMain +theory WordExamples +imports Word begin -- "modulus"