changeset 14706 | 71590b7733b7 |
parent 14589 | feae7b5fd425 |
child 15131 | c69542757a4d |
--- a/src/HOL/Library/While_Combinator.thy Thu May 06 12:43:00 2004 +0200 +++ b/src/HOL/Library/While_Combinator.thy Thu May 06 14:14:18 2004 +0200 @@ -4,10 +4,7 @@ Copyright 2000 TU Muenchen *) -header {* - \title{A general ``while'' combinator} - \author{Tobias Nipkow} -*} +header {* A general ``while'' combinator *} theory While_Combinator = Main: