changeset 6349 | f7750d816c21 |
parent 2908 | b9ba893e72cd |
child 9000 | c20d58286a51 |
6348:fdcbeaddd5fc | 6349:f7750d816c21 |
---|---|
4 Copyright |
4 Copyright |
5 |
5 |
6 Higher-order quotients. |
6 Higher-order quotients. |
7 *) |
7 *) |
8 |
8 |
9 HOL_build_completed; (*Make examples fail if HOL did*) |
|
10 |
|
11 writeln"Root file for HOL/Quot"; |
9 writeln"Root file for HOL/Quot"; |
12 |
10 |
13 use_thy "FRACT"; |
11 use_thy "FRACT"; |
14 |