src/HOL/Import/HOL/pair.imp
author obua
Wed, 28 Sep 2005 13:17:23 +0200
changeset 17694 b7870c2bd7df
parent 17658 ab7954ba5261
child 17727 83d64a461507
permissions -rw-r--r--
mapped "-->" to "hol4-->"
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
  "RPROD" > "RPROD_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     7
  "LEX" > "LEX_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     8
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     9
type_maps
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    10
  "prod" > "*"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    11
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    12
const_maps
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    13
  "pair_case" > "split"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    14
  "UNCURRY" > "split"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    15
  "SND" > "snd"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    16
  "RPROD" > "HOL4Base.pair.RPROD"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    17
  "LEX" > "HOL4Base.pair.LEX"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    18
  "FST" > "fst"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    19
  "CURRY" > "curry"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    20
  "," > "Pair"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    21
  "##" > "prod_fun"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    22
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    23
thm_maps
17694
b7870c2bd7df mapped "-->" to "hol4-->"
obua
parents: 17658
diff changeset
    24
  "pair_induction" > "Datatype.prod.induct"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    25
  "pair_case_thm" > "Product_Type.split"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    26
  "pair_case_def" > "HOL4Compat.pair_case_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    27
  "pair_case_cong" > "HOL4Base.pair.pair_case_cong"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    28
  "pair_Axiom" > "HOL4Base.pair.pair_Axiom"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    29
  "WF_RPROD" > "HOL4Base.pair.WF_RPROD"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    30
  "WF_LEX" > "HOL4Base.pair.WF_LEX"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    31
  "UNCURRY_VAR" > "Product_Type.split_beta"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    32
  "UNCURRY_ONE_ONE_THM" > "HOL4Base.pair.UNCURRY_ONE_ONE_THM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    33
  "UNCURRY_DEF" > "Product_Type.split"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    34
  "UNCURRY_CURRY_THM" > "Product_Type.split_curry"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    35
  "UNCURRY_CONG" > "HOL4Base.pair.UNCURRY_CONG"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    36
  "UNCURRY" > "Product_Type.split_beta"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    37
  "SND" > "Product_Type.snd_conv"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    38
  "RPROD_def" > "HOL4Base.pair.RPROD_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    39
  "RPROD_DEF" > "HOL4Base.pair.RPROD_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    40
  "PFORALL_THM" > "HOL4Base.pair.PFORALL_THM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    41
  "PEXISTS_THM" > "HOL4Base.pair.PEXISTS_THM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    42
  "PAIR_MAP_THM" > "Product_Type.prod_fun"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    43
  "PAIR_MAP" > "HOL4Compat.PAIR_MAP"
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 14516
diff changeset
    44
  "PAIR_EQ" > "Datatype.prod.simps_1"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    45
  "PAIR" > "HOL4Compat.PAIR"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    46
  "LEX_def" > "HOL4Base.pair.LEX_def"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    47
  "LEX_DEF" > "HOL4Base.pair.LEX_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    48
  "LET2_RATOR" > "HOL4Base.pair.LET2_RATOR"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    49
  "LET2_RAND" > "HOL4Base.pair.LET2_RAND"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    50
  "LAMBDA_PROD" > "Product_Type.split_eta"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    51
  "FST" > "Product_Type.fst_conv"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    52
  "FORALL_PROD" > "Product_Type.split_paired_All"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    53
  "EXISTS_PROD" > "Product_Type.split_paired_Ex"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    54
  "ELIM_UNCURRY" > "Product_Type.split_beta"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    55
  "ELIM_PFORALL" > "HOL4Base.pair.ELIM_PFORALL"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    56
  "ELIM_PEXISTS" > "HOL4Base.pair.ELIM_PEXISTS"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    57
  "CURRY_UNCURRY_THM" > "Product_Type.curry_split"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    58
  "CURRY_ONE_ONE_THM" > "HOL4Base.pair.CURRY_ONE_ONE_THM"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    59
  "CURRY_DEF" > "Product_Type.curry_conv"
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 14516
diff changeset
    60
  "CLOSED_PAIR_EQ" > "Datatype.prod.simps_1"
b1f486a9c56b Updated import configuration.
skalberg
parents: 14516
diff changeset
    61
  "ABS_PAIR_THM" > "Datatype.prod.nchotomy"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    62
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    63
ignore_thms
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    64
  "prod_TY_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    65
  "MK_PAIR_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    66
  "IS_PAIR_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    67
  "COMMA_DEF"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    68
  "ABS_REP_prod"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    69
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    70
end