src/HOL/Import/HOL/pair.imp
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 17916 51269a053504
child 37387 3581483cca6c
permissions -rw-r--r--
adaptions to codegen_package
     1 import
     2 
     3 import_segment "hol4"
     4 
     5 def_maps
     6   "RPROD" > "RPROD_def"
     7   "LEX" > "LEX_def"
     8 
     9 type_maps
    10   "prod" > "*"
    11 
    12 const_maps
    13   "pair_case" > "split"
    14   "UNCURRY" > "split"
    15   "SND" > "snd"
    16   "RPROD" > "HOL4Base.pair.RPROD"
    17   "LEX" > "HOL4Base.pair.LEX"
    18   "FST" > "fst"
    19   "CURRY" > "curry"
    20   "," > "Pair"
    21   "##" > "prod_fun"
    22 
    23 thm_maps
    24   "pair_induction" > "Datatype.prod.induct_correctness"
    25   "pair_case_thm" > "Product_Type.split"
    26   "pair_case_def" > "HOL4Compat.pair_case_def"
    27   "pair_case_cong" > "HOL4Base.pair.pair_case_cong"
    28   "pair_Axiom" > "HOL4Base.pair.pair_Axiom"
    29   "WF_RPROD" > "HOL4Base.pair.WF_RPROD"
    30   "WF_LEX" > "HOL4Base.pair.WF_LEX"
    31   "UNCURRY_VAR" > "Product_Type.split_beta"
    32   "UNCURRY_ONE_ONE_THM" > "HOL4Base.pair.UNCURRY_ONE_ONE_THM"
    33   "UNCURRY_DEF" > "Product_Type.split"
    34   "UNCURRY_CURRY_THM" > "Product_Type.split_curry"
    35   "UNCURRY_CONG" > "HOL4Base.pair.UNCURRY_CONG"
    36   "UNCURRY" > "Product_Type.split_beta"
    37   "SND" > "Product_Type.snd_conv"
    38   "RPROD_def" > "HOL4Base.pair.RPROD_def"
    39   "RPROD_DEF" > "HOL4Base.pair.RPROD_DEF"
    40   "PFORALL_THM" > "HOL4Base.pair.PFORALL_THM"
    41   "PEXISTS_THM" > "HOL4Base.pair.PEXISTS_THM"
    42   "PAIR_MAP_THM" > "Product_Type.prod_fun"
    43   "PAIR_MAP" > "HOL4Compat.PAIR_MAP"
    44   "PAIR_EQ" > "Datatype.prod.simps_1"
    45   "PAIR" > "HOL4Compat.PAIR"
    46   "LEX_def" > "HOL4Base.pair.LEX_def"
    47   "LEX_DEF" > "HOL4Base.pair.LEX_DEF"
    48   "LET2_RATOR" > "HOL4Base.pair.LET2_RATOR"
    49   "LET2_RAND" > "HOL4Base.pair.LET2_RAND"
    50   "LAMBDA_PROD" > "Product_Type.split_eta"
    51   "FST" > "Product_Type.fst_conv"
    52   "FORALL_PROD" > "Product_Type.split_paired_All"
    53   "EXISTS_PROD" > "Product_Type.split_paired_Ex"
    54   "ELIM_UNCURRY" > "Product_Type.split_beta"
    55   "ELIM_PFORALL" > "HOL4Base.pair.ELIM_PFORALL"
    56   "ELIM_PEXISTS" > "HOL4Base.pair.ELIM_PEXISTS"
    57   "CURRY_UNCURRY_THM" > "Product_Type.curry_split"
    58   "CURRY_ONE_ONE_THM" > "HOL4Base.pair.CURRY_ONE_ONE_THM"
    59   "CURRY_DEF" > "Product_Type.curry_conv"
    60   "CLOSED_PAIR_EQ" > "Datatype.prod.simps_1"
    61   "ABS_PAIR_THM" > "Datatype.prod.nchotomy"
    62 
    63 ignore_thms
    64   "prod_TY_DEF"
    65   "MK_PAIR_DEF"
    66   "IS_PAIR_DEF"
    67   "COMMA_DEF"
    68   "ABS_REP_prod"
    69 
    70 end