# HG changeset patch
# User wenzelm
# Date 1130531261 -7200
# Node ID d23a846598d2653f9cfbe30f2f919a6ee81e8b01
# Parent  d1ff9ebb8bcb59423f1f42fd55476330bbfcd52e
* Pure/Isar: literal facts;
* ML/Pure: tuned Thm.lift_rule;
* ML/Pure: renamed Goal constant to prop, more general uses;

diff -r d1ff9ebb8bcb -r d23a846598d2 NEWS
--- 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