src/HOL/Import/HOL/prime.imp
author wenzelm
Mon, 16 Mar 2009 18:24:30 +0100
changeset 30549 d2d7874648bd
parent 14516 a183dec876ab
permissions -rw-r--r--
simplified method setup;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     1
import
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     2
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     3
import_segment "hol4"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     4
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     5
def_maps
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     6
  "prime" > "prime_primdef"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     7
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     8
const_maps
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     9
  "prime" > "HOL4Base.prime.prime"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    10
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    11
thm_maps
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    12
  "prime_primdef" > "HOL4Base.prime.prime_primdef"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    13
  "prime_def" > "HOL4Base.prime.prime_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    14
  "NOT_PRIME_1" > "HOL4Base.prime.NOT_PRIME_1"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    15
  "NOT_PRIME_0" > "HOL4Base.prime.NOT_PRIME_0"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    16
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    17
end