# HG changeset patch
# User wenzelm
# Date 1213133318 -7200
# Node ID a1f3c7b5ce9c7a242c6e236de0447cd9259d91e9
# Parent  63fdfcf6c7a3df6e2120356f5c518879d51129b2
back to original import order -- thanks to proper deletion of nat cases/induct rules from type_definition;

diff -r 63fdfcf6c7a3 -r a1f3c7b5ce9c src/HOL/Word/WordDefinition.thy
--- a/src/HOL/Word/WordDefinition.thy	Tue Jun 10 23:28:35 2008 +0200
+++ b/src/HOL/Word/WordDefinition.thy	Tue Jun 10 23:28:38 2008 +0200
@@ -9,7 +9,7 @@
 header {* Definition of Word Type *}
 
 theory WordDefinition
-imports TdThs Size BinBoolList
+imports Size BinBoolList TdThs
 begin
 
 typedef (open word) 'a word