equal
deleted
inserted
replaced
134 within the theory header as 'abbrevs', in addition to global |
134 within the theory header as 'abbrevs', in addition to global |
135 $ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs as |
135 $ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs as |
136 before. The theory syntax for 'keywords' has been simplified |
136 before. The theory syntax for 'keywords' has been simplified |
137 accordingly: optional abbrevs need to go into the new 'abbrevs' section. |
137 accordingly: optional abbrevs need to go into the new 'abbrevs' section. |
138 |
138 |
139 |
139 * ML and document antiquotations for file-systems paths are more uniform |
140 *** Document preparation *** |
140 and diverse: |
141 |
141 |
142 * Document antiquotations for file-systems paths are more specific and |
142 @{path NAME} -- no file-system check |
143 diverse: |
143 @{file NAME} -- check for plain file |
144 |
144 @{dir NAME} -- check for directory |
145 @{path NAME} -- no check (formerly @{file_unchecked}) |
145 |
146 @{file NAME} -- plain file (formerly file or directory) |
146 Minor INCOMPATIBILITY, former uses of @{file} and @{file_unchecked} may |
147 @{dir NAME} -- directory (formerly subsumed by @{file}) |
147 have to be changed. |
148 |
|
149 Minor INCOMPATIBILITY. |
|
150 |
148 |
151 |
149 |
152 *** Isar *** |
150 *** Isar *** |
153 |
151 |
154 * The defining position of a literal fact \<open>prop\<close> is maintained more |
152 * The defining position of a literal fact \<open>prop\<close> is maintained more |