src/HOL/Import/HOL/nets.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
  "tendsto" > "tendsto_def"
skalberg@14516
     7
  "tends" > "tends_def"
skalberg@14516
     8
  "dorder" > "dorder_def"
skalberg@14516
     9
  "bounded" > "bounded_def"
skalberg@14516
    10
skalberg@14516
    11
const_maps
skalberg@14516
    12
  "tendsto" > "HOL4Real.nets.tendsto"
skalberg@14516
    13
  "tends" > "HOL4Real.nets.tends"
skalberg@14516
    14
  "dorder" > "HOL4Real.nets.dorder"
skalberg@14516
    15
  "bounded" > "HOL4Real.nets.bounded"
skalberg@14516
    16
skalberg@14516
    17
thm_maps
skalberg@14516
    18
  "tendsto_def" > "HOL4Real.nets.tendsto_def"
skalberg@14516
    19
  "tendsto" > "HOL4Real.nets.tendsto"
skalberg@14516
    20
  "tends_def" > "HOL4Real.nets.tends_def"
skalberg@14516
    21
  "tends" > "HOL4Real.nets.tends"
skalberg@14516
    22
  "dorder_def" > "HOL4Real.nets.dorder_def"
skalberg@14516
    23
  "dorder" > "HOL4Real.nets.dorder"
skalberg@14516
    24
  "bounded_def" > "HOL4Real.nets.bounded_def"
skalberg@14516
    25
  "bounded" > "HOL4Real.nets.bounded"
skalberg@14516
    26
  "SEQ_TENDS" > "HOL4Real.nets.SEQ_TENDS"
skalberg@14516
    27
  "NET_SUB" > "HOL4Real.nets.NET_SUB"
skalberg@14516
    28
  "NET_NULL_MUL" > "HOL4Real.nets.NET_NULL_MUL"
skalberg@14516
    29
  "NET_NULL_CMUL" > "HOL4Real.nets.NET_NULL_CMUL"
skalberg@14516
    30
  "NET_NULL_ADD" > "HOL4Real.nets.NET_NULL_ADD"
skalberg@14516
    31
  "NET_NULL" > "HOL4Real.nets.NET_NULL"
skalberg@14516
    32
  "NET_NEG" > "HOL4Real.nets.NET_NEG"
skalberg@14516
    33
  "NET_MUL" > "HOL4Real.nets.NET_MUL"
skalberg@14516
    34
  "NET_LE" > "HOL4Real.nets.NET_LE"
skalberg@14516
    35
  "NET_INV" > "HOL4Real.nets.NET_INV"
skalberg@14516
    36
  "NET_DIV" > "HOL4Real.nets.NET_DIV"
skalberg@14516
    37
  "NET_CONV_NZ" > "HOL4Real.nets.NET_CONV_NZ"
skalberg@14516
    38
  "NET_CONV_IBOUNDED" > "HOL4Real.nets.NET_CONV_IBOUNDED"
skalberg@14516
    39
  "NET_CONV_BOUNDED" > "HOL4Real.nets.NET_CONV_BOUNDED"
skalberg@14516
    40
  "NET_ADD" > "HOL4Real.nets.NET_ADD"
skalberg@14516
    41
  "NET_ABS" > "HOL4Real.nets.NET_ABS"
skalberg@14516
    42
  "MTOP_TENDS_UNIQ" > "HOL4Real.nets.MTOP_TENDS_UNIQ"
skalberg@14516
    43
  "MTOP_TENDS" > "HOL4Real.nets.MTOP_TENDS"
skalberg@14516
    44
  "MR1_BOUNDED" > "HOL4Real.nets.MR1_BOUNDED"
skalberg@14516
    45
  "LIM_TENDS2" > "HOL4Real.nets.LIM_TENDS2"
skalberg@14516
    46
  "LIM_TENDS" > "HOL4Real.nets.LIM_TENDS"
skalberg@14516
    47
  "DORDER_TENDSTO" > "HOL4Real.nets.DORDER_TENDSTO"
skalberg@14516
    48
  "DORDER_NGE" > "HOL4Real.nets.DORDER_NGE"
skalberg@14516
    49
  "DORDER_LEMMA" > "HOL4Real.nets.DORDER_LEMMA"
skalberg@14516
    50
skalberg@14516
    51
end