Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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 file | annotate | diff | comparison | revisions 
--- 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
isabelle