# HG changeset patch
# User paulson
# Date 1159261917 -7200
# Node ID 8b52cdaee86cc5cf5a4b5012209eb2b5389ae8b3
# Parent  384bfce59254a20e1e5e4e6ae174d6b80eaa71f7
fixed the definition of "depth"

diff -r 384bfce59254 -r 8b52cdaee86c src/HOL/ex/BT.thy
--- a/src/HOL/ex/BT.thy	Tue Sep 26 11:09:33 2006 +0200
+++ b/src/HOL/ex/BT.thy	Tue Sep 26 11:11:57 2006 +0200
@@ -3,7 +3,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
 
-Binary trees (based on the ZF version).
+Binary trees
 *)
 
 header {* Binary trees *}
@@ -35,7 +35,7 @@
 
 primrec
   "depth Lf = 0"
-  "depth (Br a t1 t2) = max (depth t1) (depth t2)"
+  "depth (Br a t1 t2) = Suc (max (depth t1) (depth t2))"
 
 primrec
   "reflect Lf = Lf"
@@ -75,8 +75,8 @@
   done
 
 lemma depth_reflect: "depth (reflect t) = depth t"
-  apply (induct t)
-   apply (simp_all add: max_ac)
+  apply (induct t) 
+   apply auto
   done
 
 text {*