Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/HOL/Import/HOL/pair.imp
author haftmann
Thu, 01 Jul 2010 16:54:44 +0200
changeset 37678 0040bafffdef
parent 37591 d3daea901123
child 40855 30d512bf47a7
permissions -rw-r--r--
"prod" and "sum" replace "*" and "+" respectively 
     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" > "Product_Type.prod"

    11 

    12 const_maps

    13   "pair_case" > "Product_Type.prod_case"

    14   "UNCURRY" > "Product_Type.prod_case"

    15   "FST" > "Product_Type.fst"

    16   "SND" > "Product_Type.snd"

    17   "RPROD" > "HOL4Base.pair.RPROD"

    18   "LEX" > "HOL4Base.pair.LEX"

    19   "CURRY" > "Product_Type.curry"

    20   "," > "Product_Type.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
wneuper/isa