# HG changeset patch
# User haftmann
# Date 1233675592 -3600
# Node ID 02e76245e5af353c32f60e8a4692e6116659c7e3
# Parent  64d41ad4ffc2416fc87b2238473366361cf61467
dropped global Nil/Append interpretation

diff -r 64d41ad4ffc2 -r 02e76245e5af src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Feb 02 13:56:24 2009 +0100
+++ b/src/HOL/List.thy	Tue Feb 03 16:39:52 2009 +0100
@@ -547,11 +547,6 @@
 lemma append_Nil2 [simp]: "xs @ [] = xs"
 by (induct xs) auto
 
-interpretation semigroup_append!: semigroup_add "op @"
-  proof qed simp
-interpretation monoid_append!: monoid_add "[]" "op @"
-  proof qed simp+
-
 lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])"
 by (induct xs) auto
 
@@ -2082,12 +2077,18 @@
 
 text{* @{const foldl} and @{text concat} *}
 
-lemma concat_conv_foldl: "concat xss = foldl op@ [] xss"
-by (induct xss) (simp_all add:monoid_append.foldl_absorb0)
-
 lemma foldl_conv_concat:
-  "foldl (op @) xs xxs = xs @ (concat xxs)"
-by(simp add:concat_conv_foldl monoid_append.foldl_absorb0)
+  "foldl (op @) xs xss = xs @ concat xss"
+proof (induct xss arbitrary: xs)
+  case Nil show ?case by simp
+next
+  interpret monoid_add "[]" "op @" proof qed simp_all
+  case Cons then show ?case by (simp add: foldl_absorb0)
+qed
+
+lemma concat_conv_foldl: "concat xss = foldl (op @) [] xss"
+  by (simp add: foldl_conv_concat)
+
 
 subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
 
diff -r 64d41ad4ffc2 -r 02e76245e5af src/HOL/MetisExamples/BT.thy
--- a/src/HOL/MetisExamples/BT.thy	Mon Feb 02 13:56:24 2009 +0100
+++ b/src/HOL/MetisExamples/BT.thy	Tue Feb 03 16:39:52 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/MetisTest/BT.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 
 Testing the metis method
@@ -181,7 +180,7 @@
 lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)"
   apply (induct t)
   apply (metis postorder.simps(1) preorder.simps(1) reflect.simps(1) rev_is_Nil_conv)
-  apply (metis Cons_eq_append_conv monoid_append.add_0_left postorder.simps(2) preorder.simps(2) reflect.simps(2) rev.simps(2) rev_append rev_rev_ident)
+  apply (metis append_Nil Cons_eq_append_conv postorder.simps(2) preorder.simps(2) reflect.simps(2) rev.simps(2) rev_append rev_rev_ident)
   done
 
 ML {*AtpWrapper.problem_name := "BT__inorder_reflect"*}