23828
|
1 |
(* Title: Pure/pure_setup.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Makarius
|
|
4 |
|
|
5 |
Pure theory setup.
|
|
6 |
*)
|
|
7 |
|
|
8 |
use_thy "Pure";
|
|
9 |
structure Pure = struct val thy = theory "Pure" end;
|
|
10 |
|
|
11 |
Context.add_setup
|
|
12 |
(Sign.del_modesyntax Syntax.default_mode Syntax.appl_syntax #>
|
|
13 |
Sign.add_syntax Syntax.applC_syntax);
|
|
14 |
use_thy "CPure";
|
|
15 |
structure CPure = struct val thy = theory "CPure" end;
|
|
16 |
|
|
17 |
use "install_pp.ML";
|
|
18 |
val use = ThyInfo.use;
|
|
19 |
val cd = File.cd o Path.explode;
|
|
20 |
ml_prompts "ML> " "ML# ";
|
|
21 |
|
|
22 |
proofs := 0;
|