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 cd "ProofGeneral"; use "ROOT.ML"; cd ".."; (* new code *) |
90 (* Next line is NEW CODE. Currently broken on SMLNJ. *) |
|
91 (* cd "ProofGeneral"; use "ROOT.ML"; cd ".."; new code *) |
91 |
92 |
92 use_thy "Pure"; |
93 use_thy "Pure"; |
93 structure Pure = struct val thy = theory "Pure" end; |
94 structure Pure = struct val thy = theory "Pure" end; |
94 |
95 |
95 Context.add_setup |
96 Context.add_setup |