tuned;
authorwenzelm
Fri Dec 23 15:21:05 2005 +0100 (2005-12-23)
changeset 185079b8b33098ced
parent 18506 96260fb11449
child 18508 c5861e128a95
tuned;
NEWS
     1.1 --- a/NEWS	Fri Dec 23 15:18:13 2005 +0100
     1.2 +++ b/NEWS	Fri Dec 23 15:21:05 2005 +0100
     1.3 @@ -169,13 +169,13 @@
     1.4  needs to be structured carefully as a two-level conjunction, using
     1.5  lists of propositions separated by 'and':
     1.6  
     1.7 -lemma
     1.8 -  shows "a : A ==> P1 a"
     1.9 -        "a : A ==> P2 a"
    1.10 -    and "b : B ==> Q1 b"
    1.11 -        "b : B ==> Q2 b"
    1.12 -        "b : B ==> Q3 b"
    1.13 -proof (induct set: A B)
    1.14 +  lemma
    1.15 +    shows "a : A ==> P1 a"
    1.16 +          "a : A ==> P2 a"
    1.17 +      and "b : B ==> Q1 b"
    1.18 +          "b : B ==> Q2 b"
    1.19 +          "b : B ==> Q3 b"
    1.20 +  proof (induct set: A B)
    1.21  
    1.22  * Provers/induct: support coinduction as well.  See
    1.23  src/HOL/Library/Coinductive_List.thy for various examples.