equal
deleted
inserted
replaced
214 proof (induct set: A B) 
214 proof (induct set: A B) 
215 
215 
216 * Provers/induct: support coinduction as well. See 
216 * Provers/induct: support coinduction as well. See 
217 src/HOL/Library/Coinductive_List.thy for various examples. 
217 src/HOL/Library/Coinductive_List.thy for various examples. 
218 
218 

219 * Simplifier: by default the simplifier trace only shows top level rewrites 

220 now. That is, trace_simp_depth_limit is set to 1 by default. Thus there is 

221 less danger of being flooded by the trace. The trace indicates where parts 

222 have been suppressed. 

223 
219 * Provers/classical: removed obsolete classical version of elim_format 
224 * Provers/classical: removed obsolete classical version of elim_format 
220 attribute; classical elim/dest rules are now treated uniformly when 
225 attribute; classical elim/dest rules are now treated uniformly when 
221 manipulating the claset. 
226 manipulating the claset. 
222 
227 
223 * Provers/classical: stricter checks to ensure that supplied intro, dest and 
228 * Provers/classical: stricter checks to ensure that supplied intro, dest and 
238 *** HOL *** 
243 *** HOL *** 
239 
244 
240 * Alternative iff syntax "A <> B" for equality on bool (with priority 
245 * Alternative iff syntax "A <> B" for equality on bool (with priority 
241 25 like >); output depends on the "iff" print_mode, the default is 
246 25 like >); output depends on the "iff" print_mode, the default is 
242 "A = B" (with priority 50). 
247 "A = B" (with priority 50). 

248 

249 * "LEAST x:A. P" expands to "LEAST x. x:A & P" (input only). 
243 
250 
244 * In the context of the assumption "~(s = t)" the Simplifier rewrites 
251 * In the context of the assumption "~(s = t)" the Simplifier rewrites 
245 "t = s" to False (by simproc "neq_simproc"). For backward 
252 "t = s" to False (by simproc "neq_simproc"). For backward 
246 compatibility this can be disabled by ML "reset use_neq_simproc". 
253 compatibility this can be disabled by ML "reset use_neq_simproc". 
247 
254 