src/HOL/Import/HOL/prime.imp
author wenzelm
Thu, 27 May 2010 18:10:37 +0200
changeset 37146 f652333bbf8e
parent 14516 a183dec876ab
permissions -rw-r--r--
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;

import

import_segment "hol4"

def_maps
  "prime" > "prime_primdef"

const_maps
  "prime" > "HOL4Base.prime.prime"

thm_maps
  "prime_primdef" > "HOL4Base.prime.prime_primdef"
  "prime_def" > "HOL4Base.prime.prime_def"
  "NOT_PRIME_1" > "HOL4Base.prime.NOT_PRIME_1"
  "NOT_PRIME_0" > "HOL4Base.prime.NOT_PRIME_0"

end