--- a/src/HOL/ex/Fundefs.thy Wed Apr 21 14:46:29 2010 +0200
+++ b/src/HOL/ex/Fundefs.thy Wed Apr 21 15:37:39 2010 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/ex/Fundefs.thy
- ID: $Id$
Author: Alexander Krauss, TU Muenchen
*)
@@ -281,17 +280,10 @@
Leaf 'a
| Branch "'a tree list"
-lemma lem:"x \<in> set l \<Longrightarrow> size x < Suc (list_size size l)"
-by (induct l, auto)
-
-function treemap :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
+fun treemap :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
where
"treemap fn (Leaf n) = (Leaf (fn n))"
| "treemap fn (Branch l) = (Branch (map (treemap fn) l))"
-by pat_completeness auto
-termination by (lexicographic_order simp:lem)
-
-declare lem[simp]
fun tinc :: "nat tree \<Rightarrow> nat tree"
where