NEWS
changeset 18674 98d380757893
parent 18644 b59766bc66c9
child 18686 cbbc71acf994
equal deleted inserted replaced
18673:fad60fe1565c 18674:98d380757893
   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