equal
deleted
inserted
replaced
130 * Document antiquotation @{file} checks file/directory entries within |
130 * Document antiquotation @{file} checks file/directory entries within |
131 the local file system. |
131 the local file system. |
132 |
132 |
133 |
133 |
134 *** HOL *** |
134 *** HOL *** |
|
135 |
|
136 * New simproc that rewrites list comprehensions applied to List.set |
|
137 to set comprehensions. |
|
138 To deactivate the simproc for historic proof scripts, use: |
|
139 |
|
140 [[simproc del: list_to_set_comprehension]] |
135 |
141 |
136 * Functions can be declared as coercions and type inference will add |
142 * Functions can be declared as coercions and type inference will add |
137 them as necessary upon input of a term. In theory Complex_Main, |
143 them as necessary upon input of a term. In theory Complex_Main, |
138 real :: nat => real and real :: int => real are declared as |
144 real :: nat => real and real :: int => real are declared as |
139 coercions. A new coercion function f is declared like this: |
145 coercions. A new coercion function f is declared like this: |