doc-src/TutorialI/Advanced/Partial.thy
changeset 17914 99ead7a7eb42
parent 15904 a6fb4ddc05c7
child 19248 25bb0a883ac5
--- a/doc-src/TutorialI/Advanced/Partial.thy	Wed Oct 19 17:21:53 2005 +0200
+++ b/doc-src/TutorialI/Advanced/Partial.thy	Wed Oct 19 21:52:07 2005 +0200
@@ -1,4 +1,4 @@
-(*<*)theory Partial = While_Combinator:(*>*)
+(*<*)theory Partial imports While_Combinator begin(*>*)
 
 text{*\noindent Throughout this tutorial, we have emphasized
 that all functions in HOL are total.  We cannot hope to define