author | wenzelm |
Wed, 23 Nov 2005 18:52:05 +0100 | |
changeset 18238 | 251bda68ba36 |
parent 18237 | 2edb6a1f9c14 |
child 18239 | 7607500220da |
--- 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