| author | wenzelm |
| Sun, 30 Jan 2011 13:02:18 +0100 | |
| changeset 41648 | 6d736d983d5c |
| parent 41589 | bbd861837ebc |
| child 46780 | ab4f3f765f91 |
| 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/GenHOL4Vec.thy |
| 41589 | 2 |
Author: Sebastian Skalberg, TU Muenchen |
|
14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
3 |
*) |
|
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
4 |
|
| 16417 | 5 |
theory GenHOL4Vec imports GenHOL4Base begin |
| 14516 | 6 |
|
7 |
import_segment "hol4"; |
|
8 |
||
9 |
setup_dump "../HOL" "HOL4Vec"; |
|
10 |
||
| 17566 | 11 |
append_dump "theory HOL4Vec imports HOL4Base begin"; |
| 14516 | 12 |
|
13 |
import_theory res_quan; |
|
14 |
end_import; |
|
15 |
||
16 |
import_theory word_base; |
|
17 |
||
18 |
const_renames |
|
19 |
BIT > bit; |
|
20 |
||
21 |
end_import; |
|
22 |
||
23 |
import_theory word_num; |
|
24 |
end_import; |
|
25 |
||
26 |
import_theory word_bitop; |
|
27 |
end_import; |
|
28 |
||
29 |
import_theory bword_num; |
|
30 |
end_import; |
|
31 |
||
32 |
import_theory bword_arith; |
|
33 |
end_import; |
|
34 |
||
35 |
import_theory bword_bitop; |
|
36 |
end_import; |
|
37 |
||
38 |
append_dump "end"; |
|
39 |
||
40 |
flush_dump; |
|
41 |
||
42 |
import_segment ""; |
|
43 |
||
44 |
end |