src/HOL/Import/HOL/relation.imp
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 14516 a183dec876ab
permissions -rw-r--r--
adaptions to codegen_package
     1 import
     2 
     3 import_segment "hol4"
     4 
     5 def_maps
     6   "transitive" > "transitive_primdef"
     7   "the_fun" > "the_fun_primdef"
     8   "pred_reflexive" > "pred_reflexive_def"
     9   "inv_image" > "inv_image_primdef"
    10   "approx" > "approx_primdef"
    11   "WFREC" > "WFREC_def"
    12   "WF" > "WF_def"
    13   "TC" > "TC_def"
    14   "RTC" > "RTC_def"
    15   "RESTRICT" > "RESTRICT_def"
    16   "RC" > "RC_primdef"
    17   "EMPTY_REL" > "EMPTY_REL_def"
    18 
    19 const_maps
    20   "transitive" > "HOL4Base.relation.transitive"
    21   "the_fun" > "HOL4Base.relation.the_fun"
    22   "pred_reflexive" > "HOL4Base.relation.pred_reflexive"
    23   "inv_image" > "HOL4Base.relation.inv_image"
    24   "approx" > "HOL4Base.relation.approx"
    25   "WFREC" > "HOL4Base.relation.WFREC"
    26   "WF" > "HOL4Base.relation.WF"
    27   "TC" > "HOL4Base.relation.TC"
    28   "RTC" > "HOL4Base.relation.RTC"
    29   "RESTRICT" > "HOL4Base.relation.RESTRICT"
    30   "RC" > "HOL4Base.relation.RC"
    31   "EMPTY_REL" > "HOL4Base.relation.EMPTY_REL"
    32 
    33 const_renames
    34   "reflexive" > "pred_reflexive"
    35 
    36 thm_maps
    37   "transitive_primdef" > "HOL4Base.relation.transitive_primdef"
    38   "transitive_def" > "HOL4Base.relation.transitive_def"
    39   "the_fun_primdef" > "HOL4Base.relation.the_fun_primdef"
    40   "the_fun_def" > "HOL4Base.relation.the_fun_def"
    41   "reflexive_def" > "HOL4Base.relation.reflexive_def"
    42   "pred_reflexive_def" > "HOL4Base.relation.pred_reflexive_def"
    43   "inv_image_primdef" > "HOL4Base.relation.inv_image_primdef"
    44   "inv_image_def" > "HOL4Base.relation.inv_image_def"
    45   "approx_primdef" > "HOL4Base.relation.approx_primdef"
    46   "approx_def" > "HOL4Base.relation.approx_def"
    47   "WF_inv_image" > "HOL4Base.relation.WF_inv_image"
    48   "WF_def" > "HOL4Base.relation.WF_def"
    49   "WF_TC" > "HOL4Base.relation.WF_TC"
    50   "WF_SUBSET" > "HOL4Base.relation.WF_SUBSET"
    51   "WF_RECURSION_THM" > "HOL4Base.relation.WF_RECURSION_THM"
    52   "WF_NOT_REFL" > "HOL4Base.relation.WF_NOT_REFL"
    53   "WF_INDUCTION_THM" > "HOL4Base.relation.WF_INDUCTION_THM"
    54   "WF_EMPTY_REL" > "HOL4Base.relation.WF_EMPTY_REL"
    55   "WF_DEF" > "HOL4Base.relation.WF_DEF"
    56   "WFREC_def" > "HOL4Base.relation.WFREC_def"
    57   "WFREC_THM" > "HOL4Base.relation.WFREC_THM"
    58   "WFREC_DEF" > "HOL4Base.relation.WFREC_DEF"
    59   "WFREC_COROLLARY" > "HOL4Base.relation.WFREC_COROLLARY"
    60   "TC_def" > "HOL4Base.relation.TC_def"
    61   "TC_TRANSITIVE" > "HOL4Base.relation.TC_TRANSITIVE"
    62   "TC_SUBSET" > "HOL4Base.relation.TC_SUBSET"
    63   "TC_STRONG_INDUCT_LEFT1" > "HOL4Base.relation.TC_STRONG_INDUCT_LEFT1"
    64   "TC_STRONG_INDUCT" > "HOL4Base.relation.TC_STRONG_INDUCT"
    65   "TC_RULES" > "HOL4Base.relation.TC_RULES"
    66   "TC_RTC" > "HOL4Base.relation.TC_RTC"
    67   "TC_RC_EQNS" > "HOL4Base.relation.TC_RC_EQNS"
    68   "TC_MONOTONE" > "HOL4Base.relation.TC_MONOTONE"
    69   "TC_INDUCT_LEFT1" > "HOL4Base.relation.TC_INDUCT_LEFT1"
    70   "TC_INDUCT" > "HOL4Base.relation.TC_INDUCT"
    71   "TC_IDEM" > "HOL4Base.relation.TC_IDEM"
    72   "TC_DEF" > "HOL4Base.relation.TC_DEF"
    73   "TC_CASES2" > "HOL4Base.relation.TC_CASES2"
    74   "TC_CASES1" > "HOL4Base.relation.TC_CASES1"
    75   "RTC_def" > "HOL4Base.relation.RTC_def"
    76   "RTC_TRANSITIVE" > "HOL4Base.relation.RTC_TRANSITIVE"
    77   "RTC_TC_RC" > "HOL4Base.relation.RTC_TC_RC"
    78   "RTC_SUBSET" > "HOL4Base.relation.RTC_SUBSET"
    79   "RTC_STRONG_INDUCT" > "HOL4Base.relation.RTC_STRONG_INDUCT"
    80   "RTC_RULES" > "HOL4Base.relation.RTC_RULES"
    81   "RTC_RTC" > "HOL4Base.relation.RTC_RTC"
    82   "RTC_REFLEXIVE" > "HOL4Base.relation.RTC_REFLEXIVE"
    83   "RTC_MONOTONE" > "HOL4Base.relation.RTC_MONOTONE"
    84   "RTC_INDUCT" > "HOL4Base.relation.RTC_INDUCT"
    85   "RTC_IDEM" > "HOL4Base.relation.RTC_IDEM"
    86   "RTC_DEF" > "HOL4Base.relation.RTC_DEF"
    87   "RTC_CASES_RTC_TWICE" > "HOL4Base.relation.RTC_CASES_RTC_TWICE"
    88   "RTC_CASES2" > "HOL4Base.relation.RTC_CASES2"
    89   "RTC_CASES1" > "HOL4Base.relation.RTC_CASES1"
    90   "RESTRICT_def" > "HOL4Base.relation.RESTRICT_def"
    91   "RESTRICT_LEMMA" > "HOL4Base.relation.RESTRICT_LEMMA"
    92   "RESTRICT_DEF" > "HOL4Base.relation.RESTRICT_DEF"
    93   "RC_primdef" > "HOL4Base.relation.RC_primdef"
    94   "RC_def" > "HOL4Base.relation.RC_def"
    95   "RC_SUBSET" > "HOL4Base.relation.RC_SUBSET"
    96   "RC_RTC" > "HOL4Base.relation.RC_RTC"
    97   "RC_REFLEXIVE" > "HOL4Base.relation.RC_REFLEXIVE"
    98   "RC_IDEM" > "HOL4Base.relation.RC_IDEM"
    99   "EMPTY_REL_def" > "HOL4Base.relation.EMPTY_REL_def"
   100   "EMPTY_REL_DEF" > "HOL4Base.relation.EMPTY_REL_DEF"
   101 
   102 end