src/HOL/Import/HOL4Compat.thy
changeset 41413 64cd30d6b0b8
parent 40607 30d512bf47a7
child 41550 efa734d9b221
     1.1 --- a/src/HOL/Import/HOL4Compat.thy	Wed Dec 29 13:51:17 2010 +0100
     1.2 +++ b/src/HOL/Import/HOL4Compat.thy	Wed Dec 29 17:34:41 2010 +0100
     1.3 @@ -3,7 +3,11 @@
     1.4  *)
     1.5  
     1.6  theory HOL4Compat
     1.7 -imports HOL4Setup Complex_Main "~~/src/HOL/Old_Number_Theory/Primes" ContNotDenum
     1.8 +imports
     1.9 +  HOL4Setup
    1.10 +  Complex_Main
    1.11 +  "~~/src/HOL/Old_Number_Theory/Primes"
    1.12 +  "~~/src/HOL/Library/ContNotDenum"
    1.13  begin
    1.14  
    1.15  abbreviation (input) mem (infixl "mem" 55) where "x mem xs \<equiv> List.member xs x"