--- a/src/HOL/Word/Word.thy Wed Apr 18 23:57:44 2012 +0200
+++ b/src/HOL/Word/Word.thy Tue Apr 17 16:21:47 2012 +1000
@@ -10,7 +10,9 @@
Misc_Typedef
"~~/src/HOL/Library/Boolean_Algebra"
Bool_List_Representation
-uses ("~~/src/HOL/Word/Tools/smt_word.ML")
+uses
+ ("~~/src/HOL/Word/Tools/smt_word.ML")
+ ("~~/src/HOL/Word/Tools/word_lib.ML")
begin
text {* see @{text "Examples/WordExamples.thy"} for examples *}
@@ -4642,7 +4644,7 @@
declare bin_to_bl_def [simp]
-
+use "~~/src/HOL/Word/Tools/word_lib.ML"
use "~~/src/HOL/Word/Tools/smt_word.ML"
setup {* SMT_Word.setup *}