changeset 46780 | ab4f3f765f91 |
parent 41589 | bbd861837ebc |
--- a/src/HOL/Import/Generate-HOL/GenHOL4Word32.thy Sat Mar 03 14:04:49 2012 +0100 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Word32.thy Sat Mar 03 21:00:04 2012 +0100 @@ -10,14 +10,14 @@ append_dump "theory HOL4Word32 imports HOL4Base begin"; -import_theory bits; +import_theory "~~/src/HOL/Import/HOL" bits; const_renames BIT > bit end_import; -import_theory word32; +import_theory "~~/src/HOL/Import/HOL" word32; const_renames "==" > EQUIV;