summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Fri, 28 Oct 2005 22:27:41 +0200 | |

changeset 18020 | d23a846598d2 |

parent 18019 | d1ff9ebb8bcb |

child 18021 | 99d170aebb6e |

* Pure/Isar: literal facts;
* ML/Pure: tuned Thm.lift_rule;
* ML/Pure: renamed Goal constant to prop, more general uses;

--- a/NEWS Fri Oct 28 22:26:10 2005 +0200 +++ b/NEWS Fri Oct 28 22:27:41 2005 +0200 @@ -43,6 +43,24 @@ This technique is potentially adventurous, depending on the facts and proof tools being involved here. +* Isar: known facts from the proof context may be specified as literal +propositions, using ASCII back-quote syntax. This works wherever +named facts used to be allowed so far, in proof commands, proof +methods, attributes etc. Literal facts are retrieved from the context +according to unification of type and term parameters. For example, +provided that "A" and "A ==> B" and "!!x. P x ==> Q x" are known +theorems in the current context, then these are valid literal facts: +`A` and `A ==> B` and `!!x. P x ==> Q x" as well as `P a ==> Q a` etc. + +There is also a proof method "fact" which does the same composition +for explicit goals states, e.g. the following proof texts coincide +with certain special cases of literal facts: + + have "A" by fact == note `A` + have "A ==> B" by fact == note `A ==> B` + have "!!x. P x ==> Q x" by fact == note `!!x. P x ==> Q x` + have "P a ==> Q a" by fact == note `P a ==> Q a` + * Input syntax now supports dummy variable binding "%_. b", where the body does not mention the bound variable. Note that dummy patterns implicitly depend on their context of bounds, which makes "{_. _}" @@ -76,6 +94,14 @@ * Library: new module Pure/General/rat.ML implementing rational numbers, replacing the former functions in the Isabelle library. +* Pure: primitive rule lift_rule now takes goal cterm instead of an +actual goal state (thm). Use Thm.lift_rule (Thm.cgoal_of st i) to +achieve the old behaviour. + +* Pure: the "Goal" constant is now called "prop", supporting a +slightly more general idea of ``protecting'' meta-level rule +statements. + * Internal goals: structure Goal provides simple interfaces for init/conclude/finish and tactical prove operations (replacing former Tactic.prove). Note that OldGoals.prove_goalw_cterm has long been