# HG changeset patch
# User krauss
# Date 1271857059 -7200
# Node ID fa30cbb455df6036aec8a62835d82f2222dadbd1
# Parent  65aabc2c89aeff186b76f431489ea2718af97bc8
simplified example

diff -r 65aabc2c89ae -r fa30cbb455df src/HOL/ex/Fundefs.thy
--- 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