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