112 resulting rule, for later use with the 'cases' method (cf. attribute 
112 resulting rule, for later use with the 'cases' method (cf. attribute 
113 case_names). 
113 case_names). 
114 
114 
115 * Isar: 'obtain' takes an optional case name for the local context 
115 * Isar: 'obtain' takes an optional case name for the local context 
116 introduction rule (default "that"). 
116 introduction rule (default "that"). 

117 

118 * Isar/locales: new derived specification elements 'definition', 

119 'abbreviation', 'axiomatization', which support typeinference, admit 

120 objectlevel specifications (equality, equivalence), and may used 

121 within an optional locale context. For example: 

122 

123 definition 

124 "f x y = x + y + 1" 

125 "g x = f x x" 

126 

127 thm f_def g_def 

128 

129 axiomatization 

130 eq (infix "===" 50) 

131 where eq_refl: "x === x" and eq_subst: "x === y ==> P x ==> P y" 

132 

133 abbreviation (output) 

134 neq (infix "=!=" 50) 

135 "(x =!= y) <> ~ (x === y)" 

136 

137 Within a locale context, constants being introduced depend on certain 

138 fixed parameters, and the constant name is qualified by the locale 

139 base name. An internal abbreviation takes care for convenient input 

140 and output, making the parameters implicit and using the original 

141 short name. Presently, abbreviations are only available "in" a target 

142 locale, but not inherited by general import expressions. 

143 

144 See the isarref manual for further details. 
117 
145 
118 * Provers/induct: improved internal context management to support 
146 * Provers/induct: improved internal context management to support 
119 local fixes and defines onthefly. Thus explicit metalevel 
147 local fixes and defines onthefly. Thus explicit metalevel 
120 connectives !! and ==> are rarely required anymore in inductive goals 
148 connectives !! and ==> are rarely required anymore in inductive goals 
121 (using objectlogic connectives for this purpose has been long 
149 (using objectlogic connectives for this purpose has been long 
361 mangling (bijective mapping from any expression values to strings). 
389 mangling (bijective mapping from any expression values to strings). 
362 
390 
363 * Pure/General/rat.ML implements rational numbers. 
391 * Pure/General/rat.ML implements rational numbers. 
364 
392 
365 * Pure/General/table.ML: the join operations now works via exceptions 
393 * Pure/General/table.ML: the join operations now works via exceptions 
366 DUP/SAME instead of type option. This is both simpler and admits 
394 DUP/SAME instead of type option. This is simpler in simple cases, and 
367 slightly more efficient complex applications. 
395 admits slightly more efficient complex applications. 
368 
396 
369 * Pure: datatype Context.generic joins theory/Proof.context and 
397 * Pure: datatype Context.generic joins theory/Proof.context and 
370 provides some facilities for code that works in either kind of 
398 provides some facilities for code that works in either kind of 
371 context, notably GenericDataFun for uniform theory and proof data. 
399 context, notably GenericDataFun for uniform theory and proof data. 
372 
400 