equal
deleted
inserted
replaced
61 text{*\noindent |
61 text{*\noindent |
62 To guarantee that the second equation can only be applied if the first |
62 To guarantee that the second equation can only be applied if the first |
63 one does not match, Isabelle internally replaces the second equation |
63 one does not match, Isabelle internally replaces the second equation |
64 by the two possibilities that are left: @{prop"sep1(a,[]) = []"} and |
64 by the two possibilities that are left: @{prop"sep1(a,[]) = []"} and |
65 @{prop"sep1(a, [x]) = [x]"}. Thus the functions @{term sep} and |
65 @{prop"sep1(a, [x]) = [x]"}. Thus the functions @{term sep} and |
66 @{term sep1} are identical. |
66 @{const sep1} are identical. |
67 |
67 |
68 \begin{warn} |
68 \begin{warn} |
69 \isacommand{recdef} only takes the first argument of a (curried) |
69 \isacommand{recdef} only takes the first argument of a (curried) |
70 recursive function into account. This means both the termination measure |
70 recursive function into account. This means both the termination measure |
71 and pattern matching can only use that first argument. In general, you will |
71 and pattern matching can only use that first argument. In general, you will |