1.1 --- a/doc-src/TutorialI/todo.tobias	Wed Oct 11 12:52:56 2000 +0200
     1.2 +++ b/doc-src/TutorialI/todo.tobias	Wed Oct 11 13:15:04 2000 +0200
     1.3 @@ -36,6 +36,8 @@
     1.4  it would be nice if @term could deal with ?-vars.
     1.5  then a number of (unchecked!) @texts could be converted to @terms.
     1.6  
     1.7 +it would be nice if one could get id to the enclosing quotes in the [source] option.
     1.8 +
     1.9  
    1.10  Minor fixes in the tutorial
    1.11  ===========================
    1.12 @@ -50,20 +52,6 @@
    1.13  
    1.14  Advanced Ind expects rulify, mp and spec. How much really?
    1.15  
    1.16 -recdef: subsection Beyond Measure on lex, finite_psubset, ...
    1.17 -incl Ackermann, which is now at the end of Recdef/termination.thy.
    1.18 --> Advanced.
    1.19 -Sentence at the end:
    1.20 -If you feel that the definition of recursive functions is overly and maybe
    1.21 -unnecessarily complicated by the requirement of totality you should ponder
    1.22 -the alternative, a logic of partial functions, where recursive definitions
    1.23 -are always wellformed. For a start, there are many
    1.24 -such logics, and no clear winner has emerged. And in all of these logics you
    1.25 -are (more or less frequently) required to reason about the definedness of
    1.26 -terms explicitly. Thus one shifts definedness arguments from definition to
    1.27 -proof time. In HOL you may have to work hard to define a function, but proofs
    1.28 -can then proceed unencumbered by worries about undefinedness.
    1.29 -
    1.30  Appendix: Lexical: long ids.
    1.31  
    1.32  Warning: infixes automatically become reserved words!