Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Import/offline/maps.lst
author paulson <lp15@cam.ac.uk>
Mon, 18 Aug 2025 22:37:21 +0100
changeset 83011 d35875d530a2
parent 81936 67ea7246a9d0
permissions -rw-r--r--
Simple facts about Lebesgue integration
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
81914
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
     1
 
T_DEF
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
     2
 
AND_DEF
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
     3
 
IMP_DEF
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
     4
 
FORALL_DEF
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
     5
 
EXISTS_DEF
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
     6
 
OR_DEF
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
     7
 
F_DEF
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
     8
 
NOT_DEF
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
     9
 
EXISTS_UNIQUE_DEF
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    10
 
_FALSITY_
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    11
 
ETA_AX        hl_ax1
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    12
 
SELECT_AX     hl_ax2
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    13
 
COND_DEF
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    14
 
DEF_o
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    15
 
I_DEF
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    16
 
TYDEF_1
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    17
 
one_DEF
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    18
 
DEF_mk_pair
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    19
 
TYDEF_prod
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    20
 
DEF_,
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    21
 
DEF_FST
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    22
 
DEF_SND
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    23
 
DEF_CURRY     -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    24
 
CURRY_DEF     CURRY_DEF
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    25
 
DEF_ONE_ONE
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    26
 
DEF_ONTO
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    27
 
INFINITY_AX   hl_ax3
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    28
 
TYDEF_num     -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    29
 
ZERO_DEF      -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    30
 
DEF_SUC       -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    31
 
SUC_DEF       -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    32
 
NOT_SUC       NOT_SUC
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    33
 
SUC_INJ       SUC_INJ
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    34
 
num_INDUCTION num_INDUCTION
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    35
 
DEF_NUMERAL
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    36
 
num_Axiom     num_Axiom
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    37
 
DEF_BIT0
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    38
 
DEF_BIT1
81936
67ea7246a9d0 more robust alignments for HOL Light Release-3.0.0;
wenzelm
parents: 81931
diff changeset 
    39
 
DEF_WF        -
67ea7246a9d0 more robust alignments for HOL Light Release-3.0.0;
wenzelm
parents: 81931
diff changeset 
    40
 
WF            WF
81914
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    41
 
DEF_PRE       -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    42
 
PRE           PRE
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    43
 
DEF_+         -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    44
 
ADD           ADD
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    45
 
DEF_*         -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    46
 
MULT          MULT
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    47
 
DEF_EXP       -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    48
 
EXP           EXP
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    49
 
DEF_<=        -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    50
 
LE            LE
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    51
 
DEF_<         -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    52
 
LT            LT
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    53
 
DEF_>=
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    54
 
DEF_>
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    55
 
DEF_MAX
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    56
 
DEF_MIN
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    57
 
DEF_EVEN      -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    58
 
EVEN          EVEN
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    59
 
DEF_-         -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    60
 
SUB           SUB
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    61
 
DEF_FACT      -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    62
 
FACT          FACT
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    63
 
DEF_DIV       -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    64
 
DEF_MOD       -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    65
 
DIVISION_0    DIVISION_0
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    66
 
TYDEF_sum     -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    67
 
DEF_INL       -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    68
 
DEF_INR       -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    69
 
sum_RECURSION sum_RECURSION
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    70
 
sum_INDUCT    sum_INDUCT
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    71
 
DEF_OUTL      -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    72
 
OUTL          OUTL
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    73
 
DEF_OUTR      -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    74
 
OUTR          OUTR
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    75
 
TYDEF_list    -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    76
 
DEF_NIL       -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    77
 
DEF_CONS      -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    78
 
list_RECURSION list_RECURSION
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    79
 
list_INDUCT   list_INDUCT
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    80
 
DEF_HD        -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    81
 
HD            HD
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    82
 
DEF_TL        -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    83
 
TL            TL
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    84
 
DEF_APPEND    -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    85
 
APPEND        APPEND
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    86
 
DEF_LENGTH    -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    87
 
LENGTH        LENGTH
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    88
 
DEF_MAP       -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    89
 
MAP           MAP
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    90
 
DEF_LAST      -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    91
 
LAST          LAST
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    92
 
TYDEF_real -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    93
 
DEF_real_of_num -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    94
 
real_of_num -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    95
 
real_of_num_th -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    96
 
DEF_real_neg -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    97
 
real_neg -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    98
 
real_neg_th -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
    99
 
DEF_real_add -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   100
 
real_add -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   101
 
real_add_th -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   102
 
DEF_real_mul -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   103
 
real_mul -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   104
 
real_mul_th -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   105
 
DEF_real_le -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   106
 
real_le -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   107
 
real_le_th -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   108
 
DEF_real_inv -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   109
 
real_inv -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   110
 
real_inv_th -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   111
 
REAL_ADD_SYM REAL_ADD_SYM
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   112
 
REAL_ADD_ASSOC REAL_ADD_ASSOC
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   113
 
REAL_ADD_LID REAL_ADD_LID
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   114
 
REAL_ADD_LINV REAL_ADD_LINV
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   115
 
REAL_MUL_SYM REAL_MUL_SYM
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   116
 
REAL_MUL_ASSOC REAL_MUL_ASSOC
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   117
 
REAL_MUL_LID REAL_MUL_LID
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   118
 
REAL_ADD_LDISTRIB REAL_ADD_LDISTRIB
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   119
 
REAL_LE_REFL REAL_LE_REFL
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   120
 
REAL_LE_ANTISYM REAL_LE_ANTISYM
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   121
 
REAL_LE_TRANS REAL_LE_TRANS
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   122
 
REAL_LE_TOTAL REAL_LE_TOTAL
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   123
 
REAL_LE_LADD_IMP REAL_LE_LADD_IMP
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   124
 
REAL_LE_MUL REAL_LE_MUL
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   125
 
REAL_OF_NUM_LE REAL_OF_NUM_LE
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   126
 
DEF_real_sub -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   127
 
real_sub real_sub
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   128
 
DEF_real_lt -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   129
 
real_lt real_lt
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   130
 
DEF_real_ge -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   131
 
real_ge real_ge
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   132
 
DEF_real_gt -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   133
 
real_gt real_gt
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   134
 
DEF_real_abs -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   135
 
real_abs real_abs
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   136
 
DEF_real_pow -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   137
 
DEF_real_div -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   138
 
real_div real_div
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   139
 
DEF_real_max -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   140
 
real_max real_max
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   141
 
DEF_real_min -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   142
 
real_min real_min
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   143
 
DEF_real_sgn -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   144
 
real_sgn real_sgn
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   145
 
REAL_HREAL_LEMMA1 -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   146
 
REAL_HREAL_LEMMA2 -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   147
 
REAL_COMPLETE_SOMEPOS REAL_COMPLETE_SOMEPOS
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   148
 
REAL_OF_NUM_MUL REAL_OF_NUM_MUL
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   149
 
REAL_OF_NUM_ADD REAL_OF_NUM_ADD
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   150
 
REAL_OF_NUM_EQ REAL_OF_NUM_EQ
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   151
 
REAL_INV_0 REAL_INV_0
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   152
 
REAL_MUL_LINV REAL_MUL_LINV
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   153
 
TYDEF_int -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   154
 
DEF_integer -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   155
 
integer integer
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   156
 
int_rep int_rep
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   157
 
int_abstr int_abstr
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   158
 
dest_int_rep dest_int_rep
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   159
 
int_eq int_eq
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   160
 
DEF_int_le -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   161
 
int_le     int_le
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   162
 
DEF_int_ge -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   163
 
int_ge     int_ge
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   164
 
DEF_int_lt -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   165
 
int_lt     int_lt
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   166
 
DEF_int_gt -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   167
 
int_gt     int_gt
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   168
 
DEF_int_of_num -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   169
 
int_of_num int_of_num
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   170
 
int_of_num_th int_of_num_th
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   171
 
int_neg    -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   172
 
int_neg_th int_neg_th
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   173
 
DEF_int_add -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   174
 
int_add    -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   175
 
int_add_th int_add_th
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   176
 
DEF_int_sub -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   177
 
int_sub    -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   178
 
int_sub_th int_sub_th
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   179
 
DEF_int_mul -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   180
 
int_mul    -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   181
 
int_mul_th int_mul_th
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   182
 
DEF_int_abs -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   183
 
int_abs    -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   184
 
int_abs_th int_abs_th
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   185
 
DEF_int_sgn -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   186
 
int_sgn    -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   187
 
int_sgn_th int_sgn_th
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   188
 
DEF_int_max -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   189
 
int_max    -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   190
 
int_max_th int_max_th
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   191
 
DEF_int_min -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   192
 
int_min    -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   193
 
int_min_th int_min_th
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   194
 
DEF_int_pow -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   195
 
int_pow    -
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   196
 
int_pow_th int_pow_th
b520eb5c8223 original HOL Light "offline" material by Cezary Kaliszyk and Alexander Krauss, from http://cl-informatik.uibk.ac.at/users/cek/import/holimport.tgz 27-Nov-2013 (37372 bytes);
wenzelm
parents:
diff changeset 
   197
 
INT_IMAGE INT_IMAGE
isabelle