src/Doc/Prog_Prove/Types_and_funs.thy
changeset 58620 7435b6a3f72e
parent 58605 9d5013661ac6
child 58860 fee7cfa69c50
     1.1 --- a/src/Doc/Prog_Prove/Types_and_funs.thy	Tue Oct 07 21:44:41 2014 +0200
     1.2 +++ b/src/Doc/Prog_Prove/Types_and_funs.thy	Tue Oct 07 22:35:11 2014 +0200
     1.3 @@ -148,7 +148,7 @@
     1.4  is measured as the number of constructors (excluding 0-ary ones, e.g., @{text
     1.5  Nil}). Lexicographic combinations are also recognized. In more complicated
     1.6  situations, the user may have to prove termination by hand. For details
     1.7 -see~\cite{Krauss}.
     1.8 +see~@{cite Krauss}.
     1.9  
    1.10  Functions defined with \isacom{fun} come with their own induction schema
    1.11  that mirrors the recursion schema and is derived from the termination