equal
deleted
inserted
replaced
38 src/Pure/ROOT0.ML or src/Pure/ROOT.ML may be opened with Isabelle/jEdit: |
38 src/Pure/ROOT0.ML or src/Pure/ROOT.ML may be opened with Isabelle/jEdit: |
39 they act like independent quasi-theories in the context of theory |
39 they act like independent quasi-theories in the context of theory |
40 ML_Bootstrap. This allows continuous checking of ML files as usual, but |
40 ML_Bootstrap. This allows continuous checking of ML files as usual, but |
41 results are isolated from the actual Isabelle/Pure that runs the IDE |
41 results are isolated from the actual Isabelle/Pure that runs the IDE |
42 itself. |
42 itself. |
|
43 |
|
44 * Highlighting of entity def/ref positions wrt. cursor. |
43 |
45 |
44 |
46 |
45 *** Isar *** |
47 *** Isar *** |
46 |
48 |
47 * Command '\<proof>' is an alias for 'sorry', with different |
49 * Command '\<proof>' is an alias for 'sorry', with different |