# HG changeset patch
# User haftmann
# Date 1180964612 -7200
# Node ID 91d71bde11121286fdc452102f5522d061908efb
# Parent  eb365b39b36d8a94d0fc221f5d504f12080b3fca
reverted appnd to append

diff -r eb365b39b36d -r 91d71bde1112 src/HOL/ex/BT.thy
--- a/src/HOL/ex/BT.thy	Mon Jun 04 15:43:31 2007 +0200
+++ b/src/HOL/ex/BT.thy	Mon Jun 04 15:43:32 2007 +0200
@@ -23,7 +23,7 @@
   preorder  :: "'a bt => 'a list"
   inorder   :: "'a bt => 'a list"
   postorder :: "'a bt => 'a list"
-  appnd     :: "'a bt => 'a bt => 'a bt"
+  append     :: "'a bt => 'a bt => 'a bt"
 
 primrec
   "n_nodes Lf = 0"
@@ -58,8 +58,8 @@
   "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
 
 primrec
-  "appnd Lf t = t"
-  "appnd (Br a t1 t2) t = Br a (appnd t1 t) (appnd t2 t)"
+  "append Lf t = t"
+  "append (Br a t1 t2) t = Br a (append t1 t) (append t2 t)"
 
 
 text {* \medskip BT simplification *}
@@ -143,29 +143,29 @@
 *}
 
 lemma append_assoc [simp]:
-     "appnd (appnd t1 t2) t3 = appnd t1 (appnd t2 t3)"
+     "append (append t1 t2) t3 = append t1 (append t2 t3)"
   apply (induct t1)
    apply simp_all
   done
 
-lemma append_Lf2 [simp]: "appnd t Lf = t"
+lemma append_Lf2 [simp]: "append t Lf = t"
   apply (induct t)
    apply simp_all
   done
 
-lemma depth_append [simp]: "depth (appnd t1 t2) = depth t1 + depth t2"
+lemma depth_append [simp]: "depth (append t1 t2) = depth t1 + depth t2"
   apply (induct t1)
    apply (simp_all add: max_add_distrib_left)
   done
 
 lemma n_leaves_append [simp]:
-     "n_leaves (appnd t1 t2) = n_leaves t1 * n_leaves t2"
+     "n_leaves (append t1 t2) = n_leaves t1 * n_leaves t2"
   apply (induct t1)
    apply (simp_all add: left_distrib)
   done
 
 lemma bt_map_append:
-     "bt_map f (appnd t1 t2) = appnd (bt_map f t1) (bt_map f t2)"
+     "bt_map f (append t1 t2) = append (bt_map f t1) (bt_map f t2)"
   apply (induct t1)
    apply simp_all
   done