equal
deleted
inserted
replaced
305 * "LEAST x:A. P" expands to "LEAST x. x:A & P" (input only). 
305 * "LEAST x:A. P" expands to "LEAST x. x:A & P" (input only). 
306 
306 
307 * In the context of the assumption "~(s = t)" the Simplifier rewrites 
307 * In the context of the assumption "~(s = t)" the Simplifier rewrites 
308 "t = s" to False (by simproc "neq_simproc"). For backward 
308 "t = s" to False (by simproc "neq_simproc"). For backward 
309 compatibility this can be disabled by ML "reset use_neq_simproc". 
309 compatibility this can be disabled by ML "reset use_neq_simproc". 

310 

311 * "m dvd n" where m and n are numbers is evaluated to True/False by simp. 
310 
312 
311 * Tactics 'sat' and 'satx' reimplemented, several improvements: goals 
313 * Tactics 'sat' and 'satx' reimplemented, several improvements: goals 
312 no longer need to be stated as "<prems> ==> False", equivalences (i.e. 
314 no longer need to be stated as "<prems> ==> False", equivalences (i.e. 
313 "=" on type bool) are handled, variable names of the form "lit_<n>" 
315 "=" on type bool) are handled, variable names of the form "lit_<n>" 
314 are no longer reserved, significant speedup. 
316 are no longer reserved, significant speedup. 