equal
deleted
inserted
replaced
7 |
7 |
8 HOLCF_build_completed; (*Cause examples to fail if HOLCF did*) |
8 HOLCF_build_completed; (*Cause examples to fail if HOLCF did*) |
9 |
9 |
10 writeln"Root file for HOLCF examples: explicit domain axiomatisation"; |
10 writeln"Root file for HOLCF examples: explicit domain axiomatisation"; |
11 proof_timing := true; |
11 proof_timing := true; |
12 time_use_thy "explicit_domains/Dnat"; |
|
13 time_use_thy "explicit_domains/Dnat2"; |
|
14 time_use_thy "explicit_domains/Stream"; |
|
15 time_use_thy "explicit_domains/Stream2"; |
|
16 time_use_thy "explicit_domains/Dlist"; |
|
17 |
12 |
18 time_use_thy "explicit_domains/Coind"; |
13 time_use_thy "Dnat"; |
19 time_use_thy "explicit_domains/Dagstuhl"; |
14 time_use_thy "Dnat2"; |
20 time_use_thy "explicit_domains/Focus_ex"; |
15 time_use_thy "Stream"; |
|
16 time_use_thy "Stream2"; |
|
17 time_use_thy "Dlist"; |
21 |
18 |
|
19 time_use_thy "Coind"; |
|
20 time_use_thy "Dagstuhl"; |
|
21 time_use_thy "Focus_ex"; |
|
22 |
|
23 cd ".."; |
22 maketest "END: Root file for HOLCF examples: explicit domain axiomatization"; |
24 maketest "END: Root file for HOLCF examples: explicit domain axiomatization"; |