src/HOL/Import/HOL/topology.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   "topology" > "topology_def"
     7   "re_universe" > "re_universe_def"
     8   "re_union" > "re_union_def"
     9   "re_subset" > "re_subset_def"
    10   "re_null" > "re_null_def"
    11   "re_intersect" > "re_intersect_def"
    12   "re_compl" > "re_compl_def"
    13   "re_Union" > "re_Union_def"
    14   "open" > "open_def"
    15   "neigh" > "neigh_def"
    16   "mtop" > "mtop_def"
    17   "mr1" > "mr1_def"
    18   "metric" > "metric_def"
    19   "limpt" > "limpt_def"
    20   "istopology" > "istopology_def"
    21   "ismet" > "ismet_def"
    22   "dist" > "dist_def"
    23   "closed" > "closed_def"
    24   "B" > "B_def"
    25 
    26 type_maps
    27   "topology" > "HOL4Real.topology.topology"
    28   "metric" > "HOL4Real.topology.metric"
    29 
    30 const_maps
    31   "re_universe" > "HOL4Real.topology.re_universe"
    32   "re_union" > "HOL4Real.topology.re_union"
    33   "re_subset" > "HOL4Real.topology.re_subset"
    34   "re_null" > "HOL4Real.topology.re_null"
    35   "re_intersect" > "HOL4Real.topology.re_intersect"
    36   "re_compl" > "HOL4Real.topology.re_compl"
    37   "re_Union" > "HOL4Real.topology.re_Union"
    38   "neigh" > "HOL4Real.topology.neigh"
    39   "mtop" > "HOL4Real.topology.mtop"
    40   "mr1" > "HOL4Real.topology.mr1"
    41   "limpt" > "HOL4Real.topology.limpt"
    42   "istopology" > "HOL4Real.topology.istopology"
    43   "ismet" > "HOL4Real.topology.ismet"
    44   "closed" > "HOL4Real.topology.closed"
    45   "B" > "HOL4Real.topology.B"
    46 
    47 thm_maps
    48   "topology_tybij" > "HOL4Real.topology.topology_tybij"
    49   "topology_TY_DEF" > "HOL4Real.topology.topology_TY_DEF"
    50   "re_universe_def" > "HOL4Real.topology.re_universe_def"
    51   "re_universe" > "HOL4Real.topology.re_universe"
    52   "re_union_def" > "HOL4Real.topology.re_union_def"
    53   "re_union" > "HOL4Real.topology.re_union"
    54   "re_subset_def" > "HOL4Real.topology.re_subset_def"
    55   "re_subset" > "HOL4Real.topology.re_subset"
    56   "re_null_def" > "HOL4Real.topology.re_null_def"
    57   "re_null" > "HOL4Real.topology.re_null"
    58   "re_intersect_def" > "HOL4Real.topology.re_intersect_def"
    59   "re_intersect" > "HOL4Real.topology.re_intersect"
    60   "re_compl_def" > "HOL4Real.topology.re_compl_def"
    61   "re_compl" > "HOL4Real.topology.re_compl"
    62   "re_Union_def" > "HOL4Real.topology.re_Union_def"
    63   "re_Union" > "HOL4Real.topology.re_Union"
    64   "neigh_def" > "HOL4Real.topology.neigh_def"
    65   "neigh" > "HOL4Real.topology.neigh"
    66   "mtop_istopology" > "HOL4Real.topology.mtop_istopology"
    67   "mtop_def" > "HOL4Real.topology.mtop_def"
    68   "mtop" > "HOL4Real.topology.mtop"
    69   "mr1_def" > "HOL4Real.topology.mr1_def"
    70   "mr1" > "HOL4Real.topology.mr1"
    71   "metric_tybij" > "HOL4Real.topology.metric_tybij"
    72   "metric_TY_DEF" > "HOL4Real.topology.metric_TY_DEF"
    73   "limpt_def" > "HOL4Real.topology.limpt_def"
    74   "limpt" > "HOL4Real.topology.limpt"
    75   "istopology_def" > "HOL4Real.topology.istopology_def"
    76   "istopology" > "HOL4Real.topology.istopology"
    77   "ismet_def" > "HOL4Real.topology.ismet_def"
    78   "ismet" > "HOL4Real.topology.ismet"
    79   "closed_def" > "HOL4Real.topology.closed_def"
    80   "closed" > "HOL4Real.topology.closed"
    81   "ball" > "HOL4Real.topology.ball"
    82   "TOPOLOGY_UNION" > "HOL4Real.topology.TOPOLOGY_UNION"
    83   "TOPOLOGY" > "HOL4Real.topology.TOPOLOGY"
    84   "SUBSET_TRANS" > "HOL4Real.topology.SUBSET_TRANS"
    85   "SUBSET_REFL" > "HOL4Real.topology.SUBSET_REFL"
    86   "SUBSET_ANTISYM" > "HOL4Real.topology.SUBSET_ANTISYM"
    87   "OPEN_UNOPEN" > "HOL4Real.topology.OPEN_UNOPEN"
    88   "OPEN_SUBOPEN" > "HOL4Real.topology.OPEN_SUBOPEN"
    89   "OPEN_OWN_NEIGH" > "HOL4Real.topology.OPEN_OWN_NEIGH"
    90   "OPEN_NEIGH" > "HOL4Real.topology.OPEN_NEIGH"
    91   "MTOP_OPEN" > "HOL4Real.topology.MTOP_OPEN"
    92   "MTOP_LIMPT" > "HOL4Real.topology.MTOP_LIMPT"
    93   "MR1_SUB_LT" > "HOL4Real.topology.MR1_SUB_LT"
    94   "MR1_SUB_LE" > "HOL4Real.topology.MR1_SUB_LE"
    95   "MR1_SUB" > "HOL4Real.topology.MR1_SUB"
    96   "MR1_LIMPT" > "HOL4Real.topology.MR1_LIMPT"
    97   "MR1_DEF" > "HOL4Real.topology.MR1_DEF"
    98   "MR1_BETWEEN1" > "HOL4Real.topology.MR1_BETWEEN1"
    99   "MR1_ADD_POS" > "HOL4Real.topology.MR1_ADD_POS"
   100   "MR1_ADD_LT" > "HOL4Real.topology.MR1_ADD_LT"
   101   "MR1_ADD" > "HOL4Real.topology.MR1_ADD"
   102   "METRIC_ZERO" > "HOL4Real.topology.METRIC_ZERO"
   103   "METRIC_TRIANGLE" > "HOL4Real.topology.METRIC_TRIANGLE"
   104   "METRIC_SYM" > "HOL4Real.topology.METRIC_SYM"
   105   "METRIC_SAME" > "HOL4Real.topology.METRIC_SAME"
   106   "METRIC_POS" > "HOL4Real.topology.METRIC_POS"
   107   "METRIC_NZ" > "HOL4Real.topology.METRIC_NZ"
   108   "METRIC_ISMET" > "HOL4Real.topology.METRIC_ISMET"
   109   "ISMET_R1" > "HOL4Real.topology.ISMET_R1"
   110   "COMPL_MEM" > "HOL4Real.topology.COMPL_MEM"
   111   "CLOSED_LIMPT" > "HOL4Real.topology.CLOSED_LIMPT"
   112   "B_def" > "HOL4Real.topology.B_def"
   113   "BALL_OPEN" > "HOL4Real.topology.BALL_OPEN"
   114   "BALL_NEIGH" > "HOL4Real.topology.BALL_NEIGH"
   115 
   116 end