NEWS
changeset 15423 761a4f8e6ad6
parent 15406 75a2ca90693e
child 15436 d059da8434a5
     1.1 --- a/NEWS	Sat Dec 18 17:12:45 2004 +0100
     1.2 +++ b/NEWS	Sat Dec 18 17:14:33 2004 +0100
     1.3 @@ -247,6 +247,14 @@
     1.4    all partial orders (class "order"), in particular numbers and sets. For
     1.5    linear orders (e.g. numbers) it treats ~ x < y just like y <= x.
     1.6  
     1.7 +  - Simproc for "let x = a in f x"
     1.8 +  If a is a free or bound variable or a constant then the let is unfolded.
     1.9 +  Otherwise first a is simplified to a', and then f a' is simplified to
    1.10 +  g. If possible we abstract a' from g arriving at "let x = a' in g' x",
    1.11 +  otherwise we unfold the let and arrive at g. The simproc can be 
    1.12 +  enabled/disabled by the reference use_let_simproc. Potential
    1.13 +  INCOMPATIBILITY since simplification is more powerful by default.
    1.14 + 
    1.15  * HOL: new 'isatool dimacs2hol' to convert files in DIMACS CNF format
    1.16    (containing Boolean satisfiability problems) into Isabelle/HOL theories.
    1.17