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