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 |
|
101 *** Isar *** |
|
102 |
|
103 * Pure: default proof step now includes 'unfold_locales'; hence |
|
104 'proof' without argument may be used to unfold locale predicates. |
99 |
105 |
100 |
106 |
101 *** Document preparation *** |
107 *** Document preparation *** |
102 |
108 |
103 * Antiquotation "lemma" takes a proposition and a simple method text as argument |
109 * Antiquotation "lemma" takes a proposition and a simple method text as argument |