equal
deleted
inserted
replaced
8 |
8 |
9 HOL_build_completed; (*Make examples fail if HOL did*) |
9 HOL_build_completed; (*Make examples fail if HOL did*) |
10 |
10 |
11 writeln"Root file for HOL/Quot"; |
11 writeln"Root file for HOL/Quot"; |
12 |
12 |
13 use_thy "Quot"; |
13 (*use_thy "Quot";*) |
|
14 |