diff -r 55c201fe4c95 -r 5ee688e36eeb NEWS
--- a/NEWS	Sun Nov 27 06:01:11 2005 +0100
+++ b/NEWS	Sun Nov 27 20:06:24 2005 +0100
@@ -67,9 +67,9 @@
 (using object-logic connectives for this purpose has been long
 obsolete anyway).  The subsequent proof patterns illustrate advanced
 techniques of natural induction; general datatypes and inductive sets
-work analogously.
-
-This is how to ``strengthen'' an inductive goal wrt. certain
+work analogously (see also src/HOL/Lambda for realistic examples).
+
+(1) This is how to ``strengthen'' an inductive goal wrt. certain
 parameters:
 
   lemma
@@ -87,10 +87,10 @@
     show ?case sorry
   qed
 
-This is how to perform induction over ``expressions of a certain
+(2) This is how to perform induction over ``expressions of a certain
 form'', using a locally defined inductive parameter n == "a x"
 together with strengthening (the latter is usually required to get
-sufficiently flexible induction hypotheses).
+sufficiently flexible induction hypotheses):
 
   lemma
     fixes a :: "'a => nat"
@@ -100,8 +100,28 @@
   proof (induct n == "a x" fixing: x)
     ...
 
-See also HOL/Isar_examples/Puzzle.thy for an application of the latter
-technique.
+See also HOL/Isar_examples/Puzzle.thy for an application of the this
+particular technique.
+
+(3) This is how to perform existential reasoning ('obtain') by
+induction, while avoiding explicit object-logic encodings:
+
+  fix n :: nat
+  obtain x :: 'a where "P n x" and "Q n x"
+  proof (induct n fixing: thesis)
+    case 0
+    obtain x where "P 0 x" and "Q 0 x" sorry
+    then show thesis by (rule "0.prems")
+  next
+    case (Suc n)
+    obtain x where "P n x" and "Q n x" by (rule Suc.hyps)
+    obtain x where "P (Suc n) x" and "Q (Suc n) x" sorry
+    then show thesis by (rule Suc.prems)
+  qed
+
+Here the 'fixing: thesis' specification essentially modifies the scope
+of the formal thesis parameter, in order to the get the whole
+existence statement through the induction as expected.
 
 * Input syntax now supports dummy variable binding "%_. b", where the
 body does not mention the bound variable.  Note that dummy patterns