equal
deleted
inserted
replaced
21 Isabelle2015). |
21 Isabelle2015). |
22 |
22 |
23 |
23 |
24 *** Prover IDE -- Isabelle/Scala/jEdit *** |
24 *** Prover IDE -- Isabelle/Scala/jEdit *** |
25 |
25 |
26 * IDE support for the Isabelle/Pure bootstrap process. The file |
26 * IDE support for the Isabelle/Pure bootstrap process. The initial files |
27 src/Pure/ROOT.ML may be opened with Isabelle/jEdit: it acts like a |
27 src/Pure/ROOT0.ML src/Pure/ROOT.ML may be opened with Isabelle/jEdit: |
28 theory body in the context of theory ML_Bootstrap. This allows |
28 they act like independent quasi-theories in the context of theory |
29 continuous checking of ML files as usual, but the result is isolated |
29 ML_Bootstrap. This allows continuous checking of ML files as usual, but |
30 from the actual Isabelle/Pure that runs the IDE itself. |
30 results are isolated from the actual Isabelle/Pure that runs the IDE |
|
31 itself. |
31 |
32 |
32 |
33 |
33 *** Isar *** |
34 *** Isar *** |
34 |
35 |
35 * Command '\<proof>' is an alias for 'sorry', with different |
36 * Command '\<proof>' is an alias for 'sorry', with different |