87 primes instead of base 26 numbers. |
87 primes instead of base 26 numbers. |
88 |
88 |
89 * Pure: new flag show_question_marks controls printing of leading |
89 * Pure: new flag show_question_marks controls printing of leading |
90 question marks in schematic variable names. |
90 question marks in schematic variable names. |
91 |
91 |
92 * Pure: new version of thms_containing that searches for a list |
92 * Pure: new version of thms_containing that searches for a list of |
93 of patterns instead of a list of constants. Available in |
93 criteria instead of a list of constants. Known criteria are: intro, |
94 ProofGeneral under ProofGeneral -> Find Theorems or C-c C-f. |
94 elim, dest, name:string, and any term. Criteria can be preceded by |
95 Example search: "(_::nat) + _ + _" "_ ==> _" |
95 '-' to select theorems that do not match. Intro, elim, dest select |
|
96 theorems that match the current goal, name:s selects theorems whose |
|
97 fully qualified name contain s. Any other term is interpreted as |
|
98 pattern and selects all theorem matching the pattern. Available in |
|
99 ProofGeneral under ProofGeneral -> Find Theorems or C-c C-f. |
|
100 |
|
101 Example: C-c C-f (100) "(_::nat) + _ + _" intro -name:"HOL." |
|
102 |
|
103 prints the last 100 theorems matching the pattern "(_::nat) + _ + _", |
|
104 matching the current goal as introduction rule and not having "HOL." |
|
105 in their name (i.e. not being defined in theory HOL). |
96 |
106 |
97 * Pure/Syntax: inner syntax includes (*(*nested*) comments*). |
107 * Pure/Syntax: inner syntax includes (*(*nested*) comments*). |
98 |
108 |
99 * Pure/Syntax: pretty pinter now supports unbreakable blocks, |
109 * Pure/Syntax: pretty pinter now supports unbreakable blocks, |
100 specified in mixfix annotations as "(00...)". |
110 specified in mixfix annotations as "(00...)". |