| changeset 46794 | b4261aa64c50 |
| parent 46788 | aefdc0095d7e |
| child 46796 | 81e5ec0a3cd0 |
--- a/src/HOL/Import/HOL_Light/Compatibility.thy Sat Mar 03 22:53:24 2012 +0100 +++ b/src/HOL/Import/HOL_Light/Compatibility.thy Sat Mar 03 23:18:23 2012 +0100 @@ -5,7 +5,7 @@ theory Compatibility imports Main Fact Parity "~~/src/HOL/Library/Infinite_Set" - HOLLightList HOLLightReal HOLLightInt "~~/src/HOL/Import/HOL4Setup" + HOLLightList HOLLightReal HOLLightInt "~~/src/HOL/Import/HOL4Syntax" begin (* list *)