equal
deleted
inserted
replaced
37 |
37 |
38 * Option to skip over proofs, using implicit 'sorry' internally. |
38 * Option to skip over proofs, using implicit 'sorry' internally. |
39 |
39 |
40 |
40 |
41 *** Pure *** |
41 *** Pure *** |
|
42 |
|
43 * Syntax translation functions (print_translation etc.) always depend |
|
44 on Proof.context. Discontinued former "(advanced)" option -- this is |
|
45 now the default. Minor INCOMPATIBILITY. |
42 |
46 |
43 * Target-sensitive commands 'interpretation' and 'sublocale'. |
47 * Target-sensitive commands 'interpretation' and 'sublocale'. |
44 Particulary, 'interpretation' now allows for non-persistent |
48 Particulary, 'interpretation' now allows for non-persistent |
45 interpretation within "context ... begin ... end" blocks. |
49 interpretation within "context ... begin ... end" blocks. |
46 See "isar-ref" manual for details. |
50 See "isar-ref" manual for details. |