src/HOL/Word/Word.thy
changeset 48891 c0eafbd55de3
parent 48196 b7313810b6e6
child 49834 b27bbb021df1
--- a/src/HOL/Word/Word.thy	Wed Aug 22 22:47:16 2012 +0200
+++ b/src/HOL/Word/Word.thy	Wed Aug 22 22:55:41 2012 +0200
@@ -10,9 +10,6 @@
   Misc_Typedef
   "~~/src/HOL/Library/Boolean_Algebra"
   Bool_List_Representation
-uses
-  ("~~/src/HOL/Word/Tools/smt_word.ML")
-  ("~~/src/HOL/Word/Tools/word_lib.ML")
 begin
 
 text {* see @{text "Examples/WordExamples.thy"} for examples *}
@@ -4647,8 +4644,8 @@
 
 declare bin_to_bl_def [simp]
 
-use "~~/src/HOL/Word/Tools/word_lib.ML"
-use "~~/src/HOL/Word/Tools/smt_word.ML"
+ML_file "~~/src/HOL/Word/Tools/word_lib.ML"
+ML_file "~~/src/HOL/Word/Tools/smt_word.ML"
 setup {* SMT_Word.setup *}
 
 hide_const (open) Word