changeset 41959 | b460124855b8 |
parent 41413 | 64cd30d6b0b8 |
child 44890 | 22f665a2e91c |
41958:5abc60a017e0 | 41959:b460124855b8 |
---|---|
1 (* Title: HOL/Library/While_Combinator.thy |
1 (* Title: HOL/ex/While_Combinator_Example.thy |
2 Author: Tobias Nipkow |
2 Author: Tobias Nipkow |
3 Copyright 2000 TU Muenchen |
3 Copyright 2000 TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 header {* An application of the While combinator *} |
6 header {* An application of the While combinator *} |