summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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