equal
deleted
inserted
replaced
33 |
33 |
34 *** Isar *** |
34 *** Isar *** |
35 |
35 |
36 * Command '\<proof>' is an alias for 'sorry', with different |
36 * Command '\<proof>' is an alias for 'sorry', with different |
37 typesetting. E.g. to produce proof holes in examples and documentation. |
37 typesetting. E.g. to produce proof holes in examples and documentation. |
|
38 |
|
39 * The old proof method "default" has been removed (legacy since |
|
40 Isabelle2016). INCOMPATIBILITY, use "standard" instead. |
38 |
41 |
39 |
42 |
40 *** HOL *** |
43 *** HOL *** |
41 |
44 |
42 * New abbreviations for negated existence (but not bounded existence): |
45 * New abbreviations for negated existence (but not bounded existence): |