equal
deleted
inserted
replaced
11 |
11 |
12 structure Readthy = ReadthyFUN (structure ThySyn = ThySyn); |
12 structure Readthy = ReadthyFUN (structure ThySyn = ThySyn); |
13 open Readthy; |
13 open Readthy; |
14 |
14 |
15 print_depth 1; |
15 print_depth 1; |
16 use_thy "cube"; |
16 use_thy "Cube"; |
17 |
17 |
18 use "../Pure/install_pp.ML"; |
18 use "../Pure/install_pp.ML"; |
19 print_depth 8; |
19 print_depth 8; |
20 |
20 |
21 val Cube_build_completed = (); (*indicate successful build*) |
21 val Cube_build_completed = (); (*indicate successful build*) |