--- a/src/HOL/Library/While_Combinator_Example.thy Sat Jan 20 00:35:10 2001 +0100
+++ b/src/HOL/Library/While_Combinator_Example.thy Sat Jan 20 00:35:35 2001 +0100
@@ -1,3 +1,4 @@
+
header {* \title{} *}
theory While_Combinator_Example = While_Combinator: