# HG changeset patch
# User wenzelm
# Date 1213127351 -7200
# Node ID 71461c77a15b7d18cb09611ba10448a72814ec78
# Parent  e26ed41cc8eab525a7738bc26e399da066c178ee
reordering of imports ensures that nat_induct stay in front;

diff -r e26ed41cc8ea -r 71461c77a15b src/HOL/Word/WordDefinition.thy
--- a/src/HOL/Word/WordDefinition.thy	Tue Jun 10 19:45:53 2008 +0200
+++ b/src/HOL/Word/WordDefinition.thy	Tue Jun 10 21:49:11 2008 +0200
@@ -9,7 +9,7 @@
 header {* Definition of Word Type *}
 
 theory WordDefinition
-imports Size BinBoolList TdThs
+imports TdThs Size BinBoolList
 begin
 
 typedef (open word) 'a word