fixed embarrassing typo in example
authorblanchet
Wed, 18 Sep 2013 15:33:31 +0200
changeset 53691 fa103abdbade
parent 53690 a3ad5a0350f9
child 53692 2c04e30c2f3e
fixed embarrassing typo in example
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 \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
       "lnull xs \<Longrightarrow> lnull ys \<Longrightarrow> 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