src/HOL/Import/HOL/pred_set.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
  "count" > "count_primdef"
skalberg@14516
     7
  "UNIV" > "UNIV_def"
skalberg@14516
     8
  "UNION" > "UNION_def"
skalberg@14516
     9
  "SURJ" > "SURJ_def"
skalberg@14516
    10
  "SUBSET" > "SUBSET_def"
skalberg@14516
    11
  "SING" > "SING_def"
skalberg@14516
    12
  "RINV" > "RINV_def"
skalberg@14516
    13
  "REST" > "REST_def"
skalberg@14516
    14
  "PSUBSET" > "PSUBSET_def"
skalberg@14516
    15
  "LINV" > "LINV_def"
skalberg@14516
    16
  "ITSET_tupled" > "ITSET_tupled_def"
skalberg@14516
    17
  "ITSET" > "ITSET_def"
skalberg@14516
    18
  "INTER" > "INTER_def"
skalberg@14516
    19
  "INSERT" > "INSERT_def"
skalberg@14516
    20
  "INJ" > "INJ_def"
skalberg@14516
    21
  "INFINITE" > "INFINITE_def"
skalberg@14516
    22
  "IMAGE" > "IMAGE_def"
skalberg@14516
    23
  "GSPEC" > "GSPEC_def"
skalberg@14516
    24
  "FINITE" > "FINITE_def"
skalberg@14516
    25
  "EMPTY" > "EMPTY_def"
skalberg@14516
    26
  "DISJOINT" > "DISJOINT_def"
skalberg@14516
    27
  "DIFF" > "DIFF_def"
skalberg@14516
    28
  "DELETE" > "DELETE_def"
skalberg@14516
    29
  "CROSS" > "CROSS_def"
skalberg@14516
    30
  "COMPL" > "COMPL_def"
skalberg@14516
    31
  "CHOICE" > "CHOICE_def"
skalberg@14516
    32
  "CARD" > "CARD_def"
skalberg@14516
    33
  "BIJ" > "BIJ_def"
skalberg@14516
    34
  "BIGUNION" > "BIGUNION_def"
skalberg@14516
    35
  "BIGINTER" > "BIGINTER_def"
skalberg@14516
    36
skalberg@14516
    37
const_maps
skalberg@14516
    38
  "count" > "HOL4Base.pred_set.count"
skalberg@14516
    39
  "UNIV" > "HOL4Base.pred_set.UNIV"
skalberg@14516
    40
  "UNION" > "HOL4Base.pred_set.UNION"
skalberg@14516
    41
  "SURJ" > "HOL4Base.pred_set.SURJ"
skalberg@14516
    42
  "SUBSET" > "HOL4Base.pred_set.SUBSET"
skalberg@14516
    43
  "SING" > "HOL4Base.pred_set.SING"
skalberg@14516
    44
  "REST" > "HOL4Base.pred_set.REST"
skalberg@14516
    45
  "PSUBSET" > "HOL4Base.pred_set.PSUBSET"
skalberg@14516
    46
  "ITSET_tupled" > "HOL4Base.pred_set.ITSET_tupled"
skalberg@14516
    47
  "ITSET" > "HOL4Base.pred_set.ITSET"
skalberg@14516
    48
  "INTER" > "HOL4Base.pred_set.INTER"
skalberg@14516
    49
  "INSERT" > "HOL4Base.pred_set.INSERT"
skalberg@14516
    50
  "INJ" > "HOL4Base.pred_set.INJ"
skalberg@14516
    51
  "INFINITE" > "HOL4Base.pred_set.INFINITE"
skalberg@14516
    52
  "IMAGE" > "HOL4Base.pred_set.IMAGE"
skalberg@14516
    53
  "FINITE" > "HOL4Base.pred_set.FINITE"
skalberg@14516
    54
  "EMPTY" > "HOL4Base.pred_set.EMPTY"
skalberg@14516
    55
  "DISJOINT" > "HOL4Base.pred_set.DISJOINT"
skalberg@14516
    56
  "DIFF" > "HOL4Base.pred_set.DIFF"
skalberg@14516
    57
  "DELETE" > "HOL4Base.pred_set.DELETE"
skalberg@14516
    58
  "CROSS" > "HOL4Base.pred_set.CROSS"
skalberg@14516
    59
  "COMPL" > "HOL4Base.pred_set.COMPL"
skalberg@14516
    60
  "BIJ" > "HOL4Base.pred_set.BIJ"
skalberg@14516
    61
  "BIGUNION" > "HOL4Base.pred_set.BIGUNION"
skalberg@14516
    62
  "BIGINTER" > "HOL4Base.pred_set.BIGINTER"
skalberg@14516
    63
skalberg@14516
    64
thm_maps
skalberg@14516
    65
  "count_primdef" > "HOL4Base.pred_set.count_primdef"
skalberg@14516
    66
  "count_def" > "HOL4Base.pred_set.count_def"
skalberg@14516
    67
  "UNIV_def" > "HOL4Base.pred_set.UNIV_def"
skalberg@14516
    68
  "UNIV_SUBSET" > "HOL4Base.pred_set.UNIV_SUBSET"
skalberg@14516
    69
  "UNIV_NOT_EMPTY" > "HOL4Base.pred_set.UNIV_NOT_EMPTY"
skalberg@14516
    70
  "UNIV_DEF" > "HOL4Base.pred_set.UNIV_DEF"
skalberg@14516
    71
  "UNION_def" > "HOL4Base.pred_set.UNION_def"
skalberg@14516
    72
  "UNION_UNIV" > "HOL4Base.pred_set.UNION_UNIV"
skalberg@14516
    73
  "UNION_SUBSET" > "HOL4Base.pred_set.UNION_SUBSET"
skalberg@14516
    74
  "UNION_OVER_INTER" > "HOL4Base.pred_set.UNION_OVER_INTER"
skalberg@14516
    75
  "UNION_IDEMPOT" > "HOL4Base.pred_set.UNION_IDEMPOT"
skalberg@14516
    76
  "UNION_EMPTY" > "HOL4Base.pred_set.UNION_EMPTY"
skalberg@14516
    77
  "UNION_DEF" > "HOL4Base.pred_set.UNION_DEF"
skalberg@14516
    78
  "UNION_COMM" > "HOL4Base.pred_set.UNION_COMM"
skalberg@14516
    79
  "UNION_ASSOC" > "HOL4Base.pred_set.UNION_ASSOC"
skalberg@14516
    80
  "SURJ_def" > "HOL4Base.pred_set.SURJ_def"
skalberg@14516
    81
  "SURJ_ID" > "HOL4Base.pred_set.SURJ_ID"
skalberg@14516
    82
  "SURJ_EMPTY" > "HOL4Base.pred_set.SURJ_EMPTY"
skalberg@14516
    83
  "SURJ_DEF" > "HOL4Base.pred_set.SURJ_DEF"
skalberg@14516
    84
  "SURJ_COMPOSE" > "HOL4Base.pred_set.SURJ_COMPOSE"
skalberg@14516
    85
  "SUBSET_def" > "HOL4Base.pred_set.SUBSET_def"
skalberg@14516
    86
  "SUBSET_UNIV" > "HOL4Base.pred_set.SUBSET_UNIV"
skalberg@14516
    87
  "SUBSET_UNION_ABSORPTION" > "HOL4Base.pred_set.SUBSET_UNION_ABSORPTION"
skalberg@14516
    88
  "SUBSET_UNION" > "HOL4Base.pred_set.SUBSET_UNION"
skalberg@14516
    89
  "SUBSET_TRANS" > "HOL4Base.pred_set.SUBSET_TRANS"
skalberg@14516
    90
  "SUBSET_REFL" > "HOL4Base.pred_set.SUBSET_REFL"
skalberg@14516
    91
  "SUBSET_INTER_ABSORPTION" > "HOL4Base.pred_set.SUBSET_INTER_ABSORPTION"
skalberg@14516
    92
  "SUBSET_INTER" > "HOL4Base.pred_set.SUBSET_INTER"
skalberg@14516
    93
  "SUBSET_INSERT_DELETE" > "HOL4Base.pred_set.SUBSET_INSERT_DELETE"
skalberg@14516
    94
  "SUBSET_INSERT" > "HOL4Base.pred_set.SUBSET_INSERT"
skalberg@14516
    95
  "SUBSET_FINITE" > "HOL4Base.pred_set.SUBSET_FINITE"
skalberg@14516
    96
  "SUBSET_EMPTY" > "HOL4Base.pred_set.SUBSET_EMPTY"
skalberg@14516
    97
  "SUBSET_DELETE" > "HOL4Base.pred_set.SUBSET_DELETE"
skalberg@14516
    98
  "SUBSET_DEF" > "HOL4Base.pred_set.SUBSET_DEF"
skalberg@14516
    99
  "SUBSET_BIGINTER" > "HOL4Base.pred_set.SUBSET_BIGINTER"
skalberg@14516
   100
  "SUBSET_ANTISYM" > "HOL4Base.pred_set.SUBSET_ANTISYM"
skalberg@14516
   101
  "SPECIFICATION" > "HOL4Base.bool.IN_DEF"
skalberg@14516
   102
  "SING_def" > "HOL4Base.pred_set.SING_def"
skalberg@14516
   103
  "SING_IFF_EMPTY_REST" > "HOL4Base.pred_set.SING_IFF_EMPTY_REST"
skalberg@14516
   104
  "SING_IFF_CARD1" > "HOL4Base.pred_set.SING_IFF_CARD1"
skalberg@14516
   105
  "SING_FINITE" > "HOL4Base.pred_set.SING_FINITE"
skalberg@14516
   106
  "SING_DELETE" > "HOL4Base.pred_set.SING_DELETE"
skalberg@14516
   107
  "SING_DEF" > "HOL4Base.pred_set.SING_DEF"
skalberg@14516
   108
  "SING" > "HOL4Base.pred_set.SING"
skalberg@14516
   109
  "SET_MINIMUM" > "HOL4Base.pred_set.SET_MINIMUM"
skalberg@14516
   110
  "SET_CASES" > "HOL4Base.pred_set.SET_CASES"
skalberg@14516
   111
  "RINV_DEF" > "HOL4Base.pred_set.RINV_DEF"
skalberg@14516
   112
  "REST_def" > "HOL4Base.pred_set.REST_def"
skalberg@14516
   113
  "REST_SUBSET" > "HOL4Base.pred_set.REST_SUBSET"
skalberg@14516
   114
  "REST_SING" > "HOL4Base.pred_set.REST_SING"
skalberg@14516
   115
  "REST_PSUBSET" > "HOL4Base.pred_set.REST_PSUBSET"
skalberg@14516
   116
  "REST_DEF" > "HOL4Base.pred_set.REST_DEF"
skalberg@14516
   117
  "PSUBSET_def" > "HOL4Base.pred_set.PSUBSET_def"
skalberg@14516
   118
  "PSUBSET_UNIV" > "HOL4Base.pred_set.PSUBSET_UNIV"
skalberg@14516
   119
  "PSUBSET_TRANS" > "HOL4Base.pred_set.PSUBSET_TRANS"
skalberg@14516
   120
  "PSUBSET_MEMBER" > "HOL4Base.pred_set.PSUBSET_MEMBER"
skalberg@14516
   121
  "PSUBSET_IRREFL" > "HOL4Base.pred_set.PSUBSET_IRREFL"
skalberg@14516
   122
  "PSUBSET_INSERT_SUBSET" > "HOL4Base.pred_set.PSUBSET_INSERT_SUBSET"
skalberg@14516
   123
  "PSUBSET_FINITE" > "HOL4Base.pred_set.PSUBSET_FINITE"
skalberg@14516
   124
  "PSUBSET_DEF" > "HOL4Base.pred_set.PSUBSET_DEF"
skalberg@14516
   125
  "NUM_SET_WOP" > "HOL4Base.pred_set.NUM_SET_WOP"
skalberg@14516
   126
  "NOT_UNIV_PSUBSET" > "HOL4Base.pred_set.NOT_UNIV_PSUBSET"
skalberg@14516
   127
  "NOT_SING_EMPTY" > "HOL4Base.pred_set.NOT_SING_EMPTY"
skalberg@14516
   128
  "NOT_PSUBSET_EMPTY" > "HOL4Base.pred_set.NOT_PSUBSET_EMPTY"
skalberg@14516
   129
  "NOT_IN_FINITE" > "HOL4Base.pred_set.NOT_IN_FINITE"
skalberg@14516
   130
  "NOT_IN_EMPTY" > "HOL4Base.pred_set.NOT_IN_EMPTY"
skalberg@14516
   131
  "NOT_INSERT_EMPTY" > "HOL4Base.pred_set.NOT_INSERT_EMPTY"
skalberg@14516
   132
  "NOT_EQUAL_SETS" > "HOL4Base.pred_set.NOT_EQUAL_SETS"
skalberg@14516
   133
  "NOT_EMPTY_SING" > "HOL4Base.pred_set.NOT_EMPTY_SING"
skalberg@14516
   134
  "NOT_EMPTY_INSERT" > "HOL4Base.pred_set.NOT_EMPTY_INSERT"
skalberg@14516
   135
  "MEMBER_NOT_EMPTY" > "HOL4Base.pred_set.MEMBER_NOT_EMPTY"
skalberg@14516
   136
  "LINV_DEF" > "HOL4Base.pred_set.LINV_DEF"
skalberg@14516
   137
  "LESS_CARD_DIFF" > "HOL4Base.pred_set.LESS_CARD_DIFF"
skalberg@14516
   138
  "ITSET_tupled_primitive_def" > "HOL4Base.pred_set.ITSET_tupled_primitive_def"
skalberg@14516
   139
  "ITSET_tupled_def" > "HOL4Base.pred_set.ITSET_tupled_def"
skalberg@14516
   140
  "ITSET_def" > "HOL4Base.pred_set.ITSET_def"
skalberg@14516
   141
  "ITSET_curried_def" > "HOL4Base.pred_set.ITSET_curried_def"
skalberg@14516
   142
  "ITSET_THM" > "HOL4Base.pred_set.ITSET_THM"
skalberg@14516
   143
  "ITSET_IND" > "HOL4Base.pred_set.ITSET_IND"
skalberg@14516
   144
  "ITSET_EMPTY" > "HOL4Base.pred_set.ITSET_EMPTY"
skalberg@14516
   145
  "IN_UNIV" > "HOL4Base.pred_set.IN_UNIV"
skalberg@14516
   146
  "IN_UNION" > "HOL4Base.pred_set.IN_UNION"
skalberg@14516
   147
  "IN_SING" > "HOL4Base.pred_set.IN_SING"
skalberg@14516
   148
  "IN_INTER" > "HOL4Base.pred_set.IN_INTER"
skalberg@14516
   149
  "IN_INSERT" > "HOL4Base.pred_set.IN_INSERT"
skalberg@14516
   150
  "IN_INFINITE_NOT_FINITE" > "HOL4Base.pred_set.IN_INFINITE_NOT_FINITE"
skalberg@14516
   151
  "IN_IMAGE" > "HOL4Base.pred_set.IN_IMAGE"
skalberg@14516
   152
  "IN_DISJOINT" > "HOL4Base.pred_set.IN_DISJOINT"
skalberg@14516
   153
  "IN_DIFF" > "HOL4Base.pred_set.IN_DIFF"
skalberg@14516
   154
  "IN_DELETE_EQ" > "HOL4Base.pred_set.IN_DELETE_EQ"
skalberg@14516
   155
  "IN_DELETE" > "HOL4Base.pred_set.IN_DELETE"
skalberg@14516
   156
  "IN_CROSS" > "HOL4Base.pred_set.IN_CROSS"
skalberg@14516
   157
  "IN_COUNT" > "HOL4Base.pred_set.IN_COUNT"
skalberg@14516
   158
  "IN_COMPL" > "HOL4Base.pred_set.IN_COMPL"
skalberg@14516
   159
  "IN_BIGUNION" > "HOL4Base.pred_set.IN_BIGUNION"
skalberg@14516
   160
  "IN_BIGINTER" > "HOL4Base.pred_set.IN_BIGINTER"
skalberg@14516
   161
  "INTER_def" > "HOL4Base.pred_set.INTER_def"
skalberg@14516
   162
  "INTER_UNIV" > "HOL4Base.pred_set.INTER_UNIV"
skalberg@14516
   163
  "INTER_UNION_COMPL" > "HOL4Base.pred_set.INTER_UNION_COMPL"
skalberg@14516
   164
  "INTER_SUBSET" > "HOL4Base.pred_set.INTER_SUBSET"
skalberg@14516
   165
  "INTER_OVER_UNION" > "HOL4Base.pred_set.INTER_OVER_UNION"
skalberg@14516
   166
  "INTER_IDEMPOT" > "HOL4Base.pred_set.INTER_IDEMPOT"
skalberg@14516
   167
  "INTER_FINITE" > "HOL4Base.pred_set.INTER_FINITE"
skalberg@14516
   168
  "INTER_EMPTY" > "HOL4Base.pred_set.INTER_EMPTY"
skalberg@14516
   169
  "INTER_DEF" > "HOL4Base.pred_set.INTER_DEF"
skalberg@14516
   170
  "INTER_COMM" > "HOL4Base.pred_set.INTER_COMM"
skalberg@14516
   171
  "INTER_ASSOC" > "HOL4Base.pred_set.INTER_ASSOC"
skalberg@14516
   172
  "INSERT_def" > "HOL4Base.pred_set.INSERT_def"
skalberg@14516
   173
  "INSERT_UNIV" > "HOL4Base.pred_set.INSERT_UNIV"
skalberg@14516
   174
  "INSERT_UNION_EQ" > "HOL4Base.pred_set.INSERT_UNION_EQ"
skalberg@14516
   175
  "INSERT_UNION" > "HOL4Base.pred_set.INSERT_UNION"
skalberg@14516
   176
  "INSERT_SUBSET" > "HOL4Base.pred_set.INSERT_SUBSET"
skalberg@14516
   177
  "INSERT_SING_UNION" > "HOL4Base.pred_set.INSERT_SING_UNION"
skalberg@14516
   178
  "INSERT_INTER" > "HOL4Base.pred_set.INSERT_INTER"
skalberg@14516
   179
  "INSERT_INSERT" > "HOL4Base.pred_set.INSERT_INSERT"
skalberg@14516
   180
  "INSERT_DIFF" > "HOL4Base.pred_set.INSERT_DIFF"
skalberg@14516
   181
  "INSERT_DELETE" > "HOL4Base.pred_set.INSERT_DELETE"
skalberg@14516
   182
  "INSERT_DEF" > "HOL4Base.pred_set.INSERT_DEF"
skalberg@14516
   183
  "INSERT_COMM" > "HOL4Base.pred_set.INSERT_COMM"
skalberg@14516
   184
  "INJ_def" > "HOL4Base.pred_set.INJ_def"
skalberg@14516
   185
  "INJ_ID" > "HOL4Base.pred_set.INJ_ID"
skalberg@14516
   186
  "INJ_EMPTY" > "HOL4Base.pred_set.INJ_EMPTY"
skalberg@14516
   187
  "INJ_DEF" > "HOL4Base.pred_set.INJ_DEF"
skalberg@14516
   188
  "INJ_COMPOSE" > "HOL4Base.pred_set.INJ_COMPOSE"
skalberg@14516
   189
  "INFINITE_def" > "HOL4Base.pred_set.INFINITE_def"
skalberg@14516
   190
  "INFINITE_UNIV" > "HOL4Base.pred_set.INFINITE_UNIV"
skalberg@14516
   191
  "INFINITE_SUBSET" > "HOL4Base.pred_set.INFINITE_SUBSET"
skalberg@14516
   192
  "INFINITE_INHAB" > "HOL4Base.pred_set.INFINITE_INHAB"
skalberg@14516
   193
  "INFINITE_DIFF_FINITE" > "HOL4Base.pred_set.INFINITE_DIFF_FINITE"
skalberg@14516
   194
  "INFINITE_DEF" > "HOL4Base.pred_set.INFINITE_DEF"
skalberg@14516
   195
  "IMAGE_def" > "HOL4Base.pred_set.IMAGE_def"
skalberg@14516
   196
  "IMAGE_UNION" > "HOL4Base.pred_set.IMAGE_UNION"
skalberg@14516
   197
  "IMAGE_SURJ" > "HOL4Base.pred_set.IMAGE_SURJ"
skalberg@14516
   198
  "IMAGE_SUBSET" > "HOL4Base.pred_set.IMAGE_SUBSET"
skalberg@14516
   199
  "IMAGE_INTER" > "HOL4Base.pred_set.IMAGE_INTER"
skalberg@14516
   200
  "IMAGE_INSERT" > "HOL4Base.pred_set.IMAGE_INSERT"
skalberg@14516
   201
  "IMAGE_IN" > "HOL4Base.pred_set.IMAGE_IN"
skalberg@14516
   202
  "IMAGE_ID" > "HOL4Base.pred_set.IMAGE_ID"
skalberg@14516
   203
  "IMAGE_FINITE" > "HOL4Base.pred_set.IMAGE_FINITE"
skalberg@14516
   204
  "IMAGE_EQ_EMPTY" > "HOL4Base.pred_set.IMAGE_EQ_EMPTY"
skalberg@14516
   205
  "IMAGE_EMPTY" > "HOL4Base.pred_set.IMAGE_EMPTY"
skalberg@14516
   206
  "IMAGE_DELETE" > "HOL4Base.pred_set.IMAGE_DELETE"
skalberg@14516
   207
  "IMAGE_DEF" > "HOL4Base.pred_set.IMAGE_DEF"
skalberg@14516
   208
  "IMAGE_COMPOSE" > "HOL4Base.pred_set.IMAGE_COMPOSE"
skalberg@14516
   209
  "IMAGE_11_INFINITE" > "HOL4Base.pred_set.IMAGE_11_INFINITE"
skalberg@14516
   210
  "GSPECIFICATION" > "HOL4Base.pred_set.GSPECIFICATION"
skalberg@14516
   211
  "FINITE_def" > "HOL4Base.pred_set.FINITE_def"
skalberg@14516
   212
  "FINITE_WEAK_ENUMERATE" > "HOL4Base.pred_set.FINITE_WEAK_ENUMERATE"
skalberg@14516
   213
  "FINITE_UNION" > "HOL4Base.pred_set.FINITE_UNION"
skalberg@14516
   214
  "FINITE_SING" > "HOL4Base.pred_set.FINITE_SING"
skalberg@14516
   215
  "FINITE_PSUBSET_UNIV" > "HOL4Base.pred_set.FINITE_PSUBSET_UNIV"
skalberg@14516
   216
  "FINITE_PSUBSET_INFINITE" > "HOL4Base.pred_set.FINITE_PSUBSET_INFINITE"
skalberg@14516
   217
  "FINITE_ISO_NUM" > "HOL4Base.pred_set.FINITE_ISO_NUM"
skalberg@14516
   218
  "FINITE_INSERT" > "HOL4Base.pred_set.FINITE_INSERT"
skalberg@14516
   219
  "FINITE_INDUCT" > "HOL4Base.pred_set.FINITE_INDUCT"
skalberg@14516
   220
  "FINITE_EMPTY" > "HOL4Base.pred_set.FINITE_EMPTY"
skalberg@14516
   221
  "FINITE_DIFF" > "HOL4Base.pred_set.FINITE_DIFF"
skalberg@14516
   222
  "FINITE_DELETE" > "HOL4Base.pred_set.FINITE_DELETE"
skalberg@14516
   223
  "FINITE_DEF" > "HOL4Base.pred_set.FINITE_DEF"
skalberg@14516
   224
  "FINITE_CROSS_EQ" > "HOL4Base.pred_set.FINITE_CROSS_EQ"
skalberg@14516
   225
  "FINITE_CROSS" > "HOL4Base.pred_set.FINITE_CROSS"
skalberg@14516
   226
  "FINITE_COUNT" > "HOL4Base.pred_set.FINITE_COUNT"
skalberg@14516
   227
  "FINITE_COMPLETE_INDUCTION" > "HOL4Base.pred_set.FINITE_COMPLETE_INDUCTION"
skalberg@14516
   228
  "FINITE_BIGUNION" > "HOL4Base.pred_set.FINITE_BIGUNION"
skalberg@14516
   229
  "EXTENSION" > "HOL4Base.pred_set.EXTENSION"
skalberg@14516
   230
  "EQ_UNIV" > "HOL4Base.pred_set.EQ_UNIV"
skalberg@14516
   231
  "EQUAL_SING" > "HOL4Base.pred_set.EQUAL_SING"
skalberg@14516
   232
  "EMPTY_def" > "HOL4Base.pred_set.EMPTY_def"
skalberg@14516
   233
  "EMPTY_UNION" > "HOL4Base.pred_set.EMPTY_UNION"
skalberg@14516
   234
  "EMPTY_SUBSET" > "HOL4Base.pred_set.EMPTY_SUBSET"
skalberg@14516
   235
  "EMPTY_NOT_UNIV" > "HOL4Base.pred_set.EMPTY_NOT_UNIV"
skalberg@14516
   236
  "EMPTY_DIFF" > "HOL4Base.pred_set.EMPTY_DIFF"
skalberg@14516
   237
  "EMPTY_DELETE" > "HOL4Base.pred_set.EMPTY_DELETE"
skalberg@14516
   238
  "EMPTY_DEF" > "HOL4Base.pred_set.EMPTY_DEF"
skalberg@14516
   239
  "DISJOINT_def" > "HOL4Base.pred_set.DISJOINT_def"
skalberg@14516
   240
  "DISJOINT_UNION_BOTH" > "HOL4Base.pred_set.DISJOINT_UNION_BOTH"
skalberg@14516
   241
  "DISJOINT_UNION" > "HOL4Base.pred_set.DISJOINT_UNION"
skalberg@14516
   242
  "DISJOINT_SYM" > "HOL4Base.pred_set.DISJOINT_SYM"
skalberg@14516
   243
  "DISJOINT_SING_EMPTY" > "HOL4Base.pred_set.DISJOINT_SING_EMPTY"
skalberg@14516
   244
  "DISJOINT_INSERT" > "HOL4Base.pred_set.DISJOINT_INSERT"
skalberg@14516
   245
  "DISJOINT_EMPTY_REFL" > "HOL4Base.pred_set.DISJOINT_EMPTY_REFL"
skalberg@14516
   246
  "DISJOINT_EMPTY" > "HOL4Base.pred_set.DISJOINT_EMPTY"
skalberg@14516
   247
  "DISJOINT_DELETE_SYM" > "HOL4Base.pred_set.DISJOINT_DELETE_SYM"
skalberg@14516
   248
  "DISJOINT_DEF" > "HOL4Base.pred_set.DISJOINT_DEF"
skalberg@14516
   249
  "DISJOINT_BIGUNION" > "HOL4Base.pred_set.DISJOINT_BIGUNION"
skalberg@14516
   250
  "DISJOINT_BIGINTER" > "HOL4Base.pred_set.DISJOINT_BIGINTER"
skalberg@14516
   251
  "DIFF_def" > "HOL4Base.pred_set.DIFF_def"
skalberg@14516
   252
  "DIFF_UNIV" > "HOL4Base.pred_set.DIFF_UNIV"
skalberg@14516
   253
  "DIFF_INSERT" > "HOL4Base.pred_set.DIFF_INSERT"
skalberg@14516
   254
  "DIFF_EQ_EMPTY" > "HOL4Base.pred_set.DIFF_EQ_EMPTY"
skalberg@14516
   255
  "DIFF_EMPTY" > "HOL4Base.pred_set.DIFF_EMPTY"
skalberg@14516
   256
  "DIFF_DIFF" > "HOL4Base.pred_set.DIFF_DIFF"
skalberg@14516
   257
  "DIFF_DEF" > "HOL4Base.pred_set.DIFF_DEF"
skalberg@14516
   258
  "DELETE_def" > "HOL4Base.pred_set.DELETE_def"
skalberg@14516
   259
  "DELETE_SUBSET" > "HOL4Base.pred_set.DELETE_SUBSET"
skalberg@14516
   260
  "DELETE_NON_ELEMENT" > "HOL4Base.pred_set.DELETE_NON_ELEMENT"
skalberg@14516
   261
  "DELETE_INTER" > "HOL4Base.pred_set.DELETE_INTER"
skalberg@14516
   262
  "DELETE_INSERT" > "HOL4Base.pred_set.DELETE_INSERT"
skalberg@14516
   263
  "DELETE_EQ_SING" > "HOL4Base.pred_set.DELETE_EQ_SING"
skalberg@14516
   264
  "DELETE_DELETE" > "HOL4Base.pred_set.DELETE_DELETE"
skalberg@14516
   265
  "DELETE_DEF" > "HOL4Base.pred_set.DELETE_DEF"
skalberg@14516
   266
  "DELETE_COMM" > "HOL4Base.pred_set.DELETE_COMM"
skalberg@14516
   267
  "DECOMPOSITION" > "HOL4Base.pred_set.DECOMPOSITION"
skalberg@14516
   268
  "CROSS_def" > "HOL4Base.pred_set.CROSS_def"
skalberg@14516
   269
  "CROSS_SUBSET" > "HOL4Base.pred_set.CROSS_SUBSET"
skalberg@14516
   270
  "CROSS_SINGS" > "HOL4Base.pred_set.CROSS_SINGS"
skalberg@14516
   271
  "CROSS_INSERT_RIGHT" > "HOL4Base.pred_set.CROSS_INSERT_RIGHT"
skalberg@14516
   272
  "CROSS_INSERT_LEFT" > "HOL4Base.pred_set.CROSS_INSERT_LEFT"
skalberg@14516
   273
  "CROSS_EMPTY" > "HOL4Base.pred_set.CROSS_EMPTY"
skalberg@14516
   274
  "CROSS_DEF" > "HOL4Base.pred_set.CROSS_DEF"
skalberg@14516
   275
  "COUNT_ZERO" > "HOL4Base.pred_set.COUNT_ZERO"
skalberg@14516
   276
  "COUNT_SUC" > "HOL4Base.pred_set.COUNT_SUC"
skalberg@14516
   277
  "COMPONENT" > "HOL4Base.pred_set.COMPONENT"
skalberg@14516
   278
  "COMPL_def" > "HOL4Base.pred_set.COMPL_def"
skalberg@14516
   279
  "COMPL_SPLITS" > "HOL4Base.pred_set.COMPL_SPLITS"
skalberg@14516
   280
  "COMPL_EMPTY" > "HOL4Base.pred_set.COMPL_EMPTY"
skalberg@14516
   281
  "COMPL_DEF" > "HOL4Base.pred_set.COMPL_DEF"
skalberg@14516
   282
  "COMPL_COMPL" > "HOL4Base.pred_set.COMPL_COMPL"
skalberg@14516
   283
  "COMPL_CLAUSES" > "HOL4Base.pred_set.COMPL_CLAUSES"
skalberg@14516
   284
  "CHOICE_SING" > "HOL4Base.pred_set.CHOICE_SING"
skalberg@14516
   285
  "CHOICE_NOT_IN_REST" > "HOL4Base.pred_set.CHOICE_NOT_IN_REST"
skalberg@14516
   286
  "CHOICE_INSERT_REST" > "HOL4Base.pred_set.CHOICE_INSERT_REST"
skalberg@14516
   287
  "CHOICE_DEF" > "HOL4Base.pred_set.CHOICE_DEF"
skalberg@14516
   288
  "CARD_UNION" > "HOL4Base.pred_set.CARD_UNION"
skalberg@14516
   289
  "CARD_SUBSET" > "HOL4Base.pred_set.CARD_SUBSET"
skalberg@14516
   290
  "CARD_SING_CROSS" > "HOL4Base.pred_set.CARD_SING_CROSS"
skalberg@14516
   291
  "CARD_SING" > "HOL4Base.pred_set.CARD_SING"
skalberg@14516
   292
  "CARD_PSUBSET" > "HOL4Base.pred_set.CARD_PSUBSET"
skalberg@14516
   293
  "CARD_INTER_LESS_EQ" > "HOL4Base.pred_set.CARD_INTER_LESS_EQ"
skalberg@14516
   294
  "CARD_INSERT" > "HOL4Base.pred_set.CARD_INSERT"
skalberg@14516
   295
  "CARD_EQ_0" > "HOL4Base.pred_set.CARD_EQ_0"
skalberg@14516
   296
  "CARD_EMPTY" > "HOL4Base.pred_set.CARD_EMPTY"
skalberg@14516
   297
  "CARD_DIFF" > "HOL4Base.pred_set.CARD_DIFF"
skalberg@14516
   298
  "CARD_DELETE" > "HOL4Base.pred_set.CARD_DELETE"
skalberg@14516
   299
  "CARD_DEF" > "HOL4Base.pred_set.CARD_DEF"
skalberg@14516
   300
  "CARD_CROSS" > "HOL4Base.pred_set.CARD_CROSS"
skalberg@14516
   301
  "CARD_COUNT" > "HOL4Base.pred_set.CARD_COUNT"
skalberg@14516
   302
  "BIJ_def" > "HOL4Base.pred_set.BIJ_def"
skalberg@14516
   303
  "BIJ_ID" > "HOL4Base.pred_set.BIJ_ID"
skalberg@14516
   304
  "BIJ_EMPTY" > "HOL4Base.pred_set.BIJ_EMPTY"
skalberg@14516
   305
  "BIJ_DEF" > "HOL4Base.pred_set.BIJ_DEF"
skalberg@14516
   306
  "BIJ_COMPOSE" > "HOL4Base.pred_set.BIJ_COMPOSE"
skalberg@14516
   307
  "BIGUNION_def" > "HOL4Base.pred_set.BIGUNION_def"
skalberg@14516
   308
  "BIGUNION_UNION" > "HOL4Base.pred_set.BIGUNION_UNION"
skalberg@14516
   309
  "BIGUNION_SUBSET" > "HOL4Base.pred_set.BIGUNION_SUBSET"
skalberg@14516
   310
  "BIGUNION_SING" > "HOL4Base.pred_set.BIGUNION_SING"
skalberg@14516
   311
  "BIGUNION_INSERT" > "HOL4Base.pred_set.BIGUNION_INSERT"
skalberg@14516
   312
  "BIGUNION_EMPTY" > "HOL4Base.pred_set.BIGUNION_EMPTY"
skalberg@14516
   313
  "BIGUNION" > "HOL4Base.pred_set.BIGUNION"
skalberg@14516
   314
  "BIGINTER_def" > "HOL4Base.pred_set.BIGINTER_def"
skalberg@14516
   315
  "BIGINTER_SING" > "HOL4Base.pred_set.BIGINTER_SING"
skalberg@14516
   316
  "BIGINTER_INTER" > "HOL4Base.pred_set.BIGINTER_INTER"
skalberg@14516
   317
  "BIGINTER_INSERT" > "HOL4Base.pred_set.BIGINTER_INSERT"
skalberg@14516
   318
  "BIGINTER_EMPTY" > "HOL4Base.pred_set.BIGINTER_EMPTY"
skalberg@14516
   319
  "BIGINTER" > "HOL4Base.pred_set.BIGINTER"
skalberg@14516
   320
  "ABSORPTION" > "HOL4Base.pred_set.ABSORPTION"
skalberg@14516
   321
skalberg@14516
   322
end