| author | wenzelm |
| Sun, 16 Jan 2011 15:53:03 +0100 | |
| changeset 41589 | bbd861837ebc |
| parent 17566 | 484ff733f29c |
| 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/GenHOL4Prob.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 GenHOL4Prob imports GenHOL4Real begin |
| 14516 | 6 |
|
7 |
import_segment "hol4"; |
|
8 |
||
9 |
setup_dump "../HOL" "HOL4Prob"; |
|
10 |
||
| 17566 | 11 |
append_dump "theory HOL4Prob imports HOL4Real begin"; |
| 14516 | 12 |
|
13 |
import_theory prob_extra; |
|
14 |
||
15 |
const_moves |
|
16 |
COMPL > GenHOL4Base.pred_set.COMPL; |
|
17 |
||
18 |
end_import; |
|
19 |
||
20 |
import_theory prob_canon; |
|
21 |
end_import; |
|
22 |
||
23 |
import_theory boolean_sequence; |
|
24 |
end_import; |
|
25 |
||
26 |
import_theory prob_algebra; |
|
27 |
end_import; |
|
28 |
||
29 |
import_theory prob; |
|
30 |
end_import; |
|
31 |
||
32 |
import_theory prob_pseudo; |
|
33 |
end_import; |
|
34 |
||
35 |
import_theory prob_indep; |
|
36 |
end_import; |
|
37 |
||
38 |
import_theory prob_uniform; |
|
39 |
end_import; |
|
40 |
||
41 |
append_dump "end"; |
|
42 |
||
43 |
flush_dump; |
|
44 |
||
45 |
import_segment ""; |
|
46 |
||
47 |
end |