theory {
  interpret {
    ###############################################################################
    # INTERPRETING HOL LIGHT NAMES INTO THE OPENTHEORY STANDARD NAMESPACE
    ###############################################################################
    
    # Global
    
    type "bool" as "bool"
    type "fun" as "->"
    type "ind" as "ind"
    const "=" as "="
    
    # Data
    
    # Data.Bool
    
    const "!" as "Data.Bool.!"
    const "/\\" as "Data.Bool./\\"
    const "==>" as "Data.Bool.==>"
    const "?" as "Data.Bool.?"
    const "?!" as "Data.Bool.?!"
    const "\\/" as "Data.Bool.\\/"
    const "~" as "Data.Bool.~"
    const "COND" as "Data.Bool.cond"
    const "F" as "Data.Bool.F"
    const "@" as "Data.Bool.select"
    const "T" as "Data.Bool.T"
    
    # Data.Function
    
    const "I" as "Data.Function.id"
    const "o" as "Data.Function.o"
    const "ONE_ONE" as "Data.Function.injective"
    const "ONTO" as "Data.Function.surjective"
    
    # Data.Pair
    
    type "prod" as "Data.Pair.*"
    
    const "," as "Data.Pair.,"
    const "FST" as "Data.Pair.fst"
    const "SND" as "Data.Pair.snd"
    
    # Data.Unit
    
    type "1" as "Data.Unit.unit"
    
    const "one" as "Data.Unit.()"
    
    # Number
    
    # Number.Natural
    
    type "num" as "Number.Natural.nat"
    
    const "+" as "Number.Natural.+"
    const "PRE" as "Number.Natural.pre"
    const "SUC" as "Number.Natural.suc"
    const "_0" as "Number.Natural.zero"
    
    # Number.Numeral
    
    const "BIT0" as "Number.Numeral.bit0"
    const "BIT1" as "Number.Numeral.bit1"
    const "NUMERAL" as "Number.Numeral.numeral"
  } in 
  article "foo.art";
}