changeset 21858 | 05f57309170c |
parent 21708 | 45e7491bea47 |
child 21889 | 682dbe947862 |
21857:f9d085c2625c | 21858:05f57309170c |
---|---|
97 structure CPure = struct val thy = theory "CPure" end; |
97 structure CPure = struct val thy = theory "CPure" end; |
98 |
98 |
99 (*final ML setup*) |
99 (*final ML setup*) |
100 use "install_pp.ML"; |
100 use "install_pp.ML"; |
101 val use = ThyInfo.use; |
101 val use = ThyInfo.use; |
102 val cd = File.cd o Path.unpack; |
102 val cd = File.cd o Path.explode; |
103 ml_prompts "ML> " "ML# "; |
103 ml_prompts "ML> " "ML# "; |
104 |
104 |
105 proofs := 0; |
105 proofs := 0; |