src/HOL/Import/HOL/num.imp
author haftmann
Tue, 08 Jun 2010 16:37:19 +0200
changeset 37387 3581483cca6c
parent 17188 a26a4fc323ed
child 44763 b50d5d694838
permissions -rw-r--r--
qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
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
type_maps
37387
3581483cca6c qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
haftmann
parents: 17188
diff changeset
     6
  "num" > "Nat.nat"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     7
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     8
const_maps
37387
3581483cca6c qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
haftmann
parents: 17188
diff changeset
     9
  "SUC" > "Nat.Suc"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    10
  "0" > "0" :: "nat"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    11
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    12
thm_maps
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    13
  "NOT_SUC" > "Nat.nat.simps_1"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    14
  "INV_SUC" > "Nat.Suc_inject"
17188
a26a4fc323ed Updated import.
obua
parents: 15647
diff changeset
    15
  "INDUCTION" > "List.lexn.induct"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    16
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    17
ignore_thms
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    18
  "num_TY_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    19
  "num_ISO_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    20
  "ZERO_REP_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    21
  "ZERO_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    22
  "SUC_REP_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    23
  "SUC_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    24
  "IS_NUM_REP"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    25
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    26
end