equal
deleted
inserted
replaced
101 Example: C-c C-f (100) "(_::nat) + _ + _" intro -name:"HOL." |
101 Example: C-c C-f (100) "(_::nat) + _ + _" intro -name:"HOL." |
102 |
102 |
103 prints the last 100 theorems matching the pattern "(_::nat) + _ + _", |
103 prints the last 100 theorems matching the pattern "(_::nat) + _ + _", |
104 matching the current goal as introduction rule and not having "HOL." |
104 matching the current goal as introduction rule and not having "HOL." |
105 in their name (i.e. not being defined in theory HOL). |
105 in their name (i.e. not being defined in theory HOL). |
|
106 |
|
107 * Pure/Syntax: In schematic variable names, *any* symbol following |
|
108 \<^isub> or \<^isup> is now treated as part of the base name. For |
|
109 example, the following works without printing of ugly ".0" indexes: |
|
110 |
|
111 lemma "x\<^isub>1 = x\<^isub>2 ==> x\<^isub>2 = x\<^isub>1" |
|
112 by simp |
106 |
113 |
107 * Pure/Syntax: inner syntax includes (*(*nested*) comments*). |
114 * Pure/Syntax: inner syntax includes (*(*nested*) comments*). |
108 |
115 |
109 * Pure/Syntax: pretty pinter now supports unbreakable blocks, |
116 * Pure/Syntax: pretty pinter now supports unbreakable blocks, |
110 specified in mixfix annotations as "(00...)". |
117 specified in mixfix annotations as "(00...)". |