changeset 46796 | 81e5ec0a3cd0 |
parent 46794 | b4261aa64c50 |
child 46798 | 9ae5c21fc88c |
--- a/src/HOL/Import/HOL4/Compatibility.thy Sat Mar 03 23:42:56 2012 +0100 +++ b/src/HOL/Import/HOL4/Compatibility.thy Sat Mar 03 23:43:21 2012 +0100 @@ -7,7 +7,7 @@ Complex_Main "~~/src/HOL/Old_Number_Theory/Primes" "~~/src/HOL/Library/ContNotDenum" - "~~/src/HOL/Import/HOL4Syntax" + "~~/src/HOL/Import/Importer" begin abbreviation (input) mem (infixl "mem" 55) where "x mem xs \<equiv> List.member xs x"