author | wenzelm |

Fri Dec 23 15:21:05 2005 +0100 (2005-12-23) | |

changeset 18507 | 9b8b33098ced |

parent 18506 | 96260fb11449 |

child 18508 | c5861e128a95 |

tuned;

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.