NEWS

 just guides the heuristic.  To find suitable measure functions, the
 termination prover sets up the goal "is_measure ?f" of the appropriate
 type and generates all solutions by prolog-style backwards proof using
 the declared rules.
 
-This setup also deals with rules like
+This setup also deals with rules like 
 
   "is_measure f ==> is_measure (list_size f)"
 
 which accommodates nested datatypes that recurse through lists.
 Similar rules are predeclared for products and option types.

 
 * Simplifier: by default the simplifier trace only shows top level
 rewrites now. That is, trace_simp_depth_limit is set to 1 by
 default. Thus there is less danger of being flooded by the trace. The
 trace indicates where parts have been suppressed.
-
+  
 * Provers/classical: removed obsolete classical version of elim_format
 attribute; classical elim/dest rules are now treated uniformly when
 manipulating the claset.
 
 * Provers/classical: stricter checks to ensure that supplied intro,

 * Method "metis" proves goals by applying the Metis general-purpose
 resolution prover (see also http://gilith.com/software/metis/).
 Examples are in the directory MetisExamples.  WARNING: the
 Isabelle/HOL-Metis integration does not yet work properly with
 multi-threading.
-
+  
 * Command 'sledgehammer' invokes external automatic theorem provers as
 background processes.  It generates calls to the "metis" method if
 successful. These can be pasted into the proof.  Users do not have to
 wait for the automatic provers to return.  WARNING: does not really
 work with multi-threading.

 for small examples, and the separate tutorial on the function
 package. The old recdef "package" is still available as before, but
 users are encouraged to use the new package.
 
 * Method "lexicographic_order" automatically synthesizes termination
-relations as lexicographic combinations of size measures.
+relations as lexicographic combinations of size measures. 
 
 * Case-expressions allow arbitrary constructor-patterns (including
 "_") and take their order into account, like in functional
 programming.  Internally, this is translated into nested
 case-expressions; missing cases are added and mapped to the predefined

 * HOL/records: generalised field-update to take a function on the
 field rather than the new value: r(|A := x|) is translated to A_update
 (K x) r The K-combinator that is internally used is called K_record.
 INCOMPATIBILITY: Usage of the plain update functions has to be
 adapted.
-
+ 
 * Class "semiring_0" now contains annihilation axioms x * 0 = 0 and 0
 * x = 0, which are required for a semiring.  Richer structures do not
 inherit from semiring_0 anymore, because this property is a theorem
 there, not an axiom.  INCOMPATIBILITY: In instances of semiring_0,
 there is more to prove, but this is mostly trivial.

   mult_pos_neg2_le   now named mult_nonneg_nonpos2
   mult_neg           now named mult_neg_neg
   mult_neg_le        now named mult_nonpos_nonpos
 
 * The following lemmas in Ring_and_Field have been added to the simplifier:
-
+     
      zero_le_square
-     not_square_less_zero
+     not_square_less_zero 
 
   The following lemmas have been deleted from Real/RealPow:
-
+  
      realpow_zero_zero
      realpow_two
      realpow_less
      zero_le_power
      realpow_two_le
      abs_realpow_two
-     realpow_two_abs
+     realpow_two_abs     
 
 * Theory Parity: added rules for simplifying exponents.
 
 * Theory List: