summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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