equal
deleted
inserted
replaced
186 * Attributes 'induct' and 'cases': type or set names may now be |
186 * Attributes 'induct' and 'cases': type or set names may now be |
187 locally fixed variables as well. |
187 locally fixed variables as well. |
188 |
188 |
189 * Isar: new syntax 'name(i-j, i-, i, ...)' for referring to specific |
189 * Isar: new syntax 'name(i-j, i-, i, ...)' for referring to specific |
190 selections of theorems in named facts via indices. |
190 selections of theorems in named facts via indices. |
|
191 |
|
192 * Pure: reorganized bootstrapping of the Pure theories; CPure is now |
|
193 derived from Pure, which contains all common declarations already. |
|
194 Both theories are defined via plain Isabelle/Isar .thy files. |
|
195 INCOMPATIBILITY: elements of CPure (such as the CPure.intro / |
|
196 CPure.elim / CPure.dest attributes) now appear in the Pure name |
|
197 space; use isatool fixcpure to adapt your theory and ML sources. |
191 |
198 |
192 |
199 |
193 *** Document preparation *** |
200 *** Document preparation *** |
194 |
201 |
195 * New antiquotations @{lhs thm} and @{rhs thm} printing the lhs/rhs of |
202 * New antiquotations @{lhs thm} and @{rhs thm} printing the lhs/rhs of |