equal
deleted
inserted
replaced
144 |
144 |
145 * Completion templates for commands involving "begin ... end" blocks, |
145 * Completion templates for commands involving "begin ... end" blocks, |
146 e.g. 'context', 'notepad'. |
146 e.g. 'context', 'notepad'. |
147 |
147 |
148 * Additional abbreviations for syntactic completion may be specified |
148 * Additional abbreviations for syntactic completion may be specified |
149 within the theory header as 'abbrevs', in addition to global |
149 within the theory header as 'abbrevs'. The theory syntax for 'keywords' |
150 $ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs as |
150 has been simplified accordingly: optional abbrevs need to go into the |
151 before. The theory syntax for 'keywords' has been simplified |
151 new 'abbrevs' section. |
152 accordingly: optional abbrevs need to go into the new 'abbrevs' section. |
152 |
|
153 * Global abbreviations via $ISABELLE_HOME/etc/abbrevs and |
|
154 $ISABELLE_HOME_USER/etc/abbrevs are no longer supported. Minor |
|
155 INCOMPATIBILITY, use 'abbrevs' within theory header instead. |
153 |
156 |
154 * ML and document antiquotations for file-systems paths are more uniform |
157 * ML and document antiquotations for file-systems paths are more uniform |
155 and diverse: |
158 and diverse: |
156 |
159 |
157 @{path NAME} -- no file-system check |
160 @{path NAME} -- no file-system check |