author | ballarin |
Fri, 13 Apr 2007 10:00:04 +0200 | |
changeset 22657 | 731622340817 |
parent 19277 | f7602e74d948 |
child 22997 | d4f3b015b50b |
permissions | -rw-r--r-- |
14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
1 |
(* Title: HOL/Import/Generate-HOL/GenHOL4Real.thy |
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
2 |
ID: $Id$ |
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
3 |
Author: Sebastian Skalberg (TU Muenchen) |
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
4 |
*) |
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
5 |
|
16417 | 6 |
theory GenHOL4Real imports GenHOL4Base begin |
14516 | 7 |
|
8 |
import_segment "hol4"; |
|
9 |
||
10 |
setup_dump "../HOL" "HOL4Real"; |
|
11 |
||
17566 | 12 |
append_dump "theory HOL4Real imports HOL4Base begin"; |
14516 | 13 |
|
14 |
import_theory realax; |
|
15 |
||
16 |
type_maps |
|
17 |
real > RealDef.real; |
|
18 |
||
19 |
const_maps |
|
20 |
real_0 > 0 :: real |
|
21 |
real_1 > 1 :: real |
|
15647 | 22 |
real_neg > uminus :: "real => real" |
23 |
inv > HOL.inverse :: "real => real" |
|
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17694
diff
changeset
|
24 |
real_add > HOL.plus :: "[real,real] => real" |
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17694
diff
changeset
|
25 |
real_mul > HOL.times :: "[real,real] => real" |
19277 | 26 |
real_lt > "Orderings.less" :: "[real,real] => bool"; |
14516 | 27 |
|
28 |
ignore_thms |
|
29 |
real_TY_DEF |
|
30 |
real_tybij |
|
31 |
real_0 |
|
32 |
real_1 |
|
33 |
real_neg |
|
34 |
real_inv |
|
35 |
real_add |
|
36 |
real_mul |
|
37 |
real_lt |
|
38 |
real_of_hreal |
|
39 |
hreal_of_real |
|
40 |
REAL_ISO_EQ |
|
41 |
REAL_POS |
|
42 |
SUP_ALLPOS_LEMMA1 |
|
43 |
SUP_ALLPOS_LEMMA2 |
|
44 |
SUP_ALLPOS_LEMMA3 |
|
45 |
SUP_ALLPOS_LEMMA4; |
|
46 |
||
47 |
end_import; |
|
48 |
||
49 |
import_theory real; |
|
50 |
||
51 |
const_maps |
|
52 |
real_gt > HOL4Compat.real_gt |
|
53 |
real_ge > HOL4Compat.real_ge |
|
19277 | 54 |
real_lte > Orderings.less_eq :: "[real,real] => bool" |
19233
77ca20b0ed77
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
17694
diff
changeset
|
55 |
real_sub > HOL.minus :: "[real,real] => real" |
15647 | 56 |
"/" > HOL.divide :: "[real,real] => real" |
57 |
pow > Nat.power :: "[real,nat] => real" |
|
58 |
abs > HOL.abs :: "real => real" |
|
59 |
real_of_num > RealDef.real :: "nat => real"; |
|
14516 | 60 |
|
61 |
end_import; |
|
62 |
||
63 |
import_theory topology; |
|
64 |
end_import; |
|
65 |
||
66 |
import_theory nets; |
|
67 |
end_import; |
|
68 |
||
69 |
import_theory seq; |
|
17694 | 70 |
const_renames |
71 |
"-->" > "hol4-->"; |
|
72 |
||
14516 | 73 |
end_import; |
74 |
||
75 |
import_theory lim; |
|
76 |
end_import; |
|
77 |
||
78 |
import_theory powser; |
|
79 |
end_import; |
|
80 |
||
81 |
import_theory transc; |
|
82 |
end_import; |
|
83 |
||
84 |
import_theory poly; |
|
85 |
end_import; |
|
86 |
||
87 |
append_dump "end"; |
|
88 |
||
89 |
flush_dump; |
|
90 |
||
91 |
import_segment ""; |
|
92 |
||
93 |
end |