doc-src/isac/chuber/bakk_thesis_prelim.tex
branchdecompose-isar
changeset 42147 dc6853589935
parent 42144 f098153f2273
     1.1 --- a/doc-src/isac/chuber/bakk_thesis_prelim.tex	Thu Jul 21 16:47:34 2011 +0200
     1.2 +++ b/doc-src/isac/chuber/bakk_thesis_prelim.tex	Thu Jul 21 17:03:45 2011 +0200
     1.3 @@ -34,7 +34,7 @@
     1.4  
     1.5  The goal of this thesis is generation of interactive course material on FP and respective theory of programming, implemented in Isabelle and \sisac.
     1.6  
     1.7 -The material shall use most recent developments, for instance the ``function package'' \cite{krauss:funs} recently implemented in Isabelle. This package supports all what is needed for programming and proving properties of programs.
     1.8 +The material shall use most recent developments, for instance the ``function package'' \cite{krauss:funs,krauss:termination07,krauss:partial06} recently implemented in Isabelle. This package supports all what is needed for programming and proving properties of programs.
     1.9  
    1.10  Although addressing most recent developments and theory at the state of the art, the material also shall serve in early phases of programming. Experience shows, that in early phases (in analogy to doing mathematics \cite{?}) proceeding step by step in a program is important for learning. This will be done by implementing selected programs into \sisac.
    1.11