| author | skalberg |
| Sat, 17 Apr 2004 23:53:35 +0200 | |
| changeset 14620 | 1be590fd2422 |
| parent 14516 | a183dec876ab |
| child 15647 | b1f486a9c56b |
| 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 |
|
| 14516 | 6 |
theory GenHOL4Real = GenHOL4Base: |
7 |
||
8 |
import_segment "hol4"; |
|
9 |
||
10 |
setup_dump "../HOL" "HOL4Real"; |
|
11 |
||
12 |
append_dump "theory HOL4Real = HOL4Base:"; |
|
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 |
|
22 |
real_neg > uminus :: "real \<Rightarrow> real" |
|
23 |
inv > HOL.inverse :: "real \<Rightarrow> real" |
|
24 |
real_add > "op +" :: "[real,real] \<Rightarrow> real" |
|
25 |
real_mul > "op *" :: "[real,real] \<Rightarrow> real" |
|
26 |
real_lt > "op <" :: "[real,real] \<Rightarrow> bool"; |
|
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 |
|
54 |
real_lte > "op <=" :: "[real,real] \<Rightarrow> bool" |
|
55 |
real_sub > "op -" :: "[real,real] \<Rightarrow> real" |
|
56 |
"/" > HOL.divide :: "[real,real] \<Rightarrow> real" |
|
57 |
pow > Nat.power :: "[real,nat] \<Rightarrow> real" |
|
58 |
abs > HOL.abs :: "real \<Rightarrow> real" |
|
59 |
real_of_num > RealDef.real :: "nat \<Rightarrow> real"; |
|
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; |
|
70 |
end_import; |
|
71 |
||
72 |
import_theory lim; |
|
73 |
end_import; |
|
74 |
||
75 |
import_theory powser; |
|
76 |
end_import; |
|
77 |
||
78 |
import_theory transc; |
|
79 |
end_import; |
|
80 |
||
81 |
import_theory poly; |
|
82 |
end_import; |
|
83 |
||
84 |
append_dump "end"; |
|
85 |
||
86 |
flush_dump; |
|
87 |
||
88 |
import_segment ""; |
|
89 |
||
90 |
end |