equal
deleted
inserted
replaced
95 * Command '\<proof>' is an alias for 'sorry', with different |
95 * Command '\<proof>' is an alias for 'sorry', with different |
96 typesetting. E.g. to produce proof holes in examples and documentation. |
96 typesetting. E.g. to produce proof holes in examples and documentation. |
97 |
97 |
98 * The old proof method "default" has been removed (legacy since |
98 * The old proof method "default" has been removed (legacy since |
99 Isabelle2016). INCOMPATIBILITY, use "standard" instead. |
99 Isabelle2016). INCOMPATIBILITY, use "standard" instead. |
|
100 |
|
101 * Proof methods may refer to the main facts via the dynamic fact |
|
102 "method_facts". This is particularly useful for Eisbach method |
|
103 definitions. |
|
104 |
|
105 * Eisbach provides method "use" to modify the main facts of a given |
|
106 method expression, e.g. |
|
107 |
|
108 (use facts in simp) |
|
109 (use facts in \<open>simp add: ...\<close>) |
100 |
110 |
101 |
111 |
102 *** Pure *** |
112 *** Pure *** |
103 |
113 |
104 * Code generator: config option "code_timing" triggers measurements of |
114 * Code generator: config option "code_timing" triggers measurements of |