equal
deleted
inserted
replaced
1 (*<*)theory Partial = While_Combinator:(*>*) |
1 (*<*)theory Partial imports While_Combinator begin(*>*) |
2 |
2 |
3 text{*\noindent Throughout this tutorial, we have emphasized |
3 text{*\noindent Throughout this tutorial, we have emphasized |
4 that all functions in HOL are total. We cannot hope to define |
4 that all functions in HOL are total. We cannot hope to define |
5 truly partial functions, but must make them total. A straightforward |
5 truly partial functions, but must make them total. A straightforward |
6 method is to lift the result type of the function from $\tau$ to |
6 method is to lift the result type of the function from $\tau$ to |