Provers/induct: definitional insts and fixing;
authorwenzelm
Wed, 23 Nov 2005 18:52:05 +0100
changeset 18238 251bda68ba36
parent 18237 2edb6a1f9c14
child 18239 7607500220da
Provers/induct: definitional insts and fixing;
NEWS
--- a/NEWS	Wed Nov 23 18:52:04 2005 +0100
+++ b/NEWS	Wed Nov 23 18:52:05 2005 +0100
@@ -70,7 +70,8 @@
 work analogously.
 
 This is how to ``strengthen'' an inductive goal wrt. certain
-parameters:
+parameters (the scope of the internal generalization is both the goal
+and any additional facts being inserted before induction):
 
   lemma
     fixes n :: nat and x :: 'a