equal
deleted
inserted
replaced
84 |
84 |
85 (*configuration for Proof General*) |
85 (*configuration for Proof General*) |
86 (* Next line is OLD CODE: in case you have problems, uncomment next line and |
86 (* Next line is OLD CODE: in case you have problems, uncomment next line and |
87 comment out line after. Please report any problems to da@inf.ed.ac.uk. |
87 comment out line after. Please report any problems to da@inf.ed.ac.uk. |
88 Plan is to remove old code very soon. *) |
88 Plan is to remove old code very soon. *) |
89 (use |> setmp proofs 1 |> setmp quick_and_dirty true) "proof_general.ML"; |
89 (*(use |> setmp proofs 1 |> setmp quick_and_dirty true) "proof_general.ML"; *) |
90 (* Next line is NEW CODE. Currently broken on SMLNJ. *) |
90 (* Next line is NEW CODE. Hopefully now working on SMLNJ and Poly/ML. *) |
91 (* cd "ProofGeneral"; use "ROOT.ML"; cd ".."; new code *) |
91 cd "ProofGeneral"; use "ROOT.ML"; cd ".."; |
92 |
92 |
93 use_thy "Pure"; |
93 use_thy "Pure"; |
94 structure Pure = struct val thy = theory "Pure" end; |
94 structure Pure = struct val thy = theory "Pure" end; |
95 |
95 |
96 Context.add_setup |
96 Context.add_setup |