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