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