150 The symbol \<some> is displayed as the alternative epsilon of LaTeX |
150 The symbol \<some> is displayed as the alternative epsilon of LaTeX |
151 and x-symbol; use option '-m epsilon' to get it actually printed. |
151 and x-symbol; use option '-m epsilon' to get it actually printed. |
152 Moreover, the mathematically important symbolic identifier |
152 Moreover, the mathematically important symbolic identifier |
153 \<epsilon> becomes available as variable, constant etc. |
153 \<epsilon> becomes available as variable, constant etc. |
154 |
154 |
155 * HOL: Summation over nat with syntax '\<Sum>i<k. e' is now just a |
155 * HOL/SetInterval: The syntax for open intervals has changed: |
156 translation into 'setsum'. |
156 |
|
157 Old New |
|
158 {..n(} -> {..<n} |
|
159 {)n..} -> {n<..} |
|
160 {m..n(} -> {m..<n} |
|
161 {)m..n} -> {m<..n} |
|
162 {)m..n(} -> {m<..<n} |
|
163 |
|
164 The old syntax is still supported but will disappear in the future. |
|
165 For conversion use the following emacs search and replace patterns: |
|
166 |
|
167 {)\([^\.]*\)\.\. -> {\1<\.\.} |
|
168 \.\.\([^(}]*\)(} -> \.\.<\1} |
|
169 |
|
170 They are not perfect but work quite well. |
|
171 |
|
172 * HOL: There is new syntax for summation over finite sets: |
|
173 |
|
174 '\<Sum>x | P. e' is the same as 'setsum (%x. e) {x. P}' |
|
175 '\<Sum>x<k. e' is the same as 'setsum (%x. e) {..<k}' |
|
176 |
|
177 Function 'Summation' over nat is gone, its syntax '\<Sum>i<k. e' |
|
178 now translates into 'setsum' as above. |
|
179 |
157 |
180 |
158 *** HOLCF *** |
181 *** HOLCF *** |
159 |
182 |
160 * HOLCF: discontinued special version of 'constdefs' (which used to |
183 * HOLCF: discontinued special version of 'constdefs' (which used to |
161 support continuous functions) in favor of the general Pure one with |
184 support continuous functions) in favor of the general Pure one with |