| changeset 46796 | 81e5ec0a3cd0 |
| parent 46794 | b4261aa64c50 |
| child 46798 | 9ae5c21fc88c |
--- a/src/HOL/Import/HOL_Light/Compatibility.thy Sat Mar 03 23:42:56 2012 +0100 +++ b/src/HOL/Import/HOL_Light/Compatibility.thy Sat Mar 03 23:43:21 2012 +0100 @@ -5,7 +5,7 @@ theory Compatibility imports Main Fact Parity "~~/src/HOL/Library/Infinite_Set" - HOLLightList HOLLightReal HOLLightInt "~~/src/HOL/Import/HOL4Syntax" + HOLLightList HOLLightReal HOLLightInt "~~/src/HOL/Import/Importer" begin (* list *)