summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Fri, 23 Dec 2005 15:21:05 +0100 | |

changeset 18507 | 9b8b33098ced |

parent 18506 | 96260fb11449 |

child 18508 | c5861e128a95 |

tuned;

--- a/NEWS Fri Dec 23 15:18:13 2005 +0100 +++ b/NEWS Fri Dec 23 15:21:05 2005 +0100 @@ -169,13 +169,13 @@ needs to be structured carefully as a two-level conjunction, using lists of propositions separated by 'and': -lemma - shows "a : A ==> P1 a" - "a : A ==> P2 a" - and "b : B ==> Q1 b" - "b : B ==> Q2 b" - "b : B ==> Q3 b" -proof (induct set: A B) + lemma + shows "a : A ==> P1 a" + "a : A ==> P2 a" + and "b : B ==> Q1 b" + "b : B ==> Q2 b" + "b : B ==> Q3 b" + proof (induct set: A B) * Provers/induct: support coinduction as well. See src/HOL/Library/Coinductive_List.thy for various examples.