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 Cc Cf. 
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 Cc Cf. 

100 

101 Example: Cc Cf (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...)". 