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 *** Document preparation *** |
|
102 |
|
103 * Antiquotation "lemma" takes a proposition and a simple method text as argument |
|
104 and asserts that the proposition is provable by the corresponding method |
|
105 invocation. Prints text of proposition, as does antiquotation "prop". A simple |
|
106 method text is either a method name or a method name plus (optional) method |
|
107 arguments in parentheses, mimicing the conventions known from Isar proof text. |
|
108 Useful for illustration of presented theorems by particular examples. |
99 |
109 |
100 |
110 |
101 *** HOL *** |
111 *** HOL *** |
102 |
112 |
103 * Merged theories Wellfounded_Recursion, Accessible_Part and Wellfounded_Relations |
113 * Merged theories Wellfounded_Recursion, Accessible_Part and Wellfounded_Relations |