author | kleing |
Mon, 29 Dec 2003 06:49:26 +0100 | |
changeset 14333 | 14f29eb097a3 |
parent 13439 | 2f98365f57a8 |
child 16417 | 9bc16273c2d4 |
permissions | -rw-r--r-- |
theory FP0 = PreList: datatype 'a list = Nil ("[]") | Cons 'a "'a list" (infixr "#" 65) consts app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65) rev :: "'a list \<Rightarrow> 'a list" primrec "[] @ ys = ys" "(x # xs) @ ys = x # (xs @ ys)" primrec "rev [] = []" "rev (x # xs) = (rev xs) @ (x # [])" theorem rev_rev [simp]: "rev(rev xs) = xs" (*<*)oops(*>*)text_raw{*\isanewline\isanewline*} end