# HG changeset patch # User blanchet # Date 1379511211 -7200 # Node ID fa103abdbadeb1549f033975b8d163b6db544ed0 # Parent a3ad5a0350f909c49a59c9f052c7b019b950e7cb fixed embarrassing typo in example diff -r a3ad5a0350f9 -r fa103abdbade src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Wed Sep 18 15:33:30 2013 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Wed Sep 18 15:33:31 2013 +0200 @@ -1721,7 +1721,7 @@ primcorec lappend :: "'a llist \ 'a llist \ 'a llist" where "lnull xs \ lnull ys \ lnull (lappend xs ys)" | "lhd (lappend xs ys) = lhd (if lnull xs then ys else xs)" | - "ltl (lappend xs ys) = ltl (if lnull xs then ys else xs)" + "ltl (lappend xs ys) = (if xs = LNil then ltl ys else lappend (ltl xs) ys)" . (*<*) end