equal
deleted
inserted
replaced
94 * Indexing of literal facts: be more serious about including only |
94 * Indexing of literal facts: be more serious about including only |
95 facts from the visible specification/proof context, but not the |
95 facts from the visible specification/proof context, but not the |
96 background context (locale etc.). Affects `prop` notation and method |
96 background context (locale etc.). Affects `prop` notation and method |
97 "fact". INCOMPATIBILITY: need to name facts explicitly in rare |
97 "fact". INCOMPATIBILITY: need to name facts explicitly in rare |
98 situations. |
98 situations. |
|
99 |
|
100 * Method "cases", "induct", "coinduct": removed obsolete/undocumented |
|
101 "(open)" option, which used to expose internal bound variables to the |
|
102 proof text. |
|
103 |
|
104 * Isar statements: removed obsolete case "rule_context". |
|
105 INCOMPATIBILITY, better use explicit fixes/assumes. |
99 |
106 |
100 * Locale proofs: default proof step now includes 'unfold_locales'; |
107 * Locale proofs: default proof step now includes 'unfold_locales'; |
101 hence 'proof' without argument may be used to unfold locale |
108 hence 'proof' without argument may be used to unfold locale |
102 predicates. |
109 predicates. |
103 |
110 |