equal
deleted
inserted
replaced
1 |
1 |
2 Sequents_build_completed; (*Cause examples to fail if Sequents did*) |
2 Sequents_build_completed; (*Cause examples to fail if Sequents did*) |
3 writeln"Root file for ILL examples"; |
3 writeln"Root file for ILL examples"; |
4 |
4 |
5 proof_timing := true; |
5 set proof_timing; |
|
6 |
6 time_use_thy "ILL/washing"; |
7 time_use_thy "ILL/washing"; |
7 |
8 |
8 time_use_thy "ILL/ILL_predlog"; |
9 time_use_thy "ILL/ILL_predlog"; |
9 time_use "ILL/ILL_kleene_lemmas.ML"; |
10 time_use "ILL/ILL_kleene_lemmas.ML"; |
10 |
|
11 maketest"END: Root file for ILL examples"; |
|