# HG changeset patch
# User paulson
# Date 1195835876 -3600
# Node ID ba2bcae7aafdf59d1758e72a713e6276595f6051
# Parent  6f79698f294df13edfba9c790df18a545570c81e
faster metis calls

diff -r 6f79698f294d -r ba2bcae7aafd src/HOL/MetisExamples/BT.thy
--- a/src/HOL/MetisExamples/BT.thy	Thu Nov 22 14:51:34 2007 +0100
+++ b/src/HOL/MetisExamples/BT.thy	Fri Nov 23 17:37:56 2007 +0100
@@ -171,7 +171,7 @@
 lemma n_leaves_bt_map [simp]: "n_leaves (bt_map f t) = n_leaves t"
   apply (induct t)
   apply (metis One_nat_def Suc_eq_add_numeral_1 bt_map.simps(1) less_add_one less_antisym linorder_neq_iff n_leaves.simps(1))
-  apply (metis add_commute bt_map.simps(2) n_leaves.simps(2))
+  apply (metis bt_map.simps(2) n_leaves.simps(2))
   done
 
 
@@ -179,7 +179,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 append_eq_append_conv2 inorder.simps(1) postorder.simps(2) preorder.simps(2) reflect.simps(2) rev_append rev_is_rev_conv rev_singleton_conv rev_swap rotate_simps)
+  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)
   done
 
 ML {*ResAtp.problem_name := "BT__inorder_reflect"*}
@@ -193,7 +193,7 @@
 lemma postorder_reflect: "postorder (reflect t) = rev (preorder t)"
   apply (induct t)
   apply (metis postorder.simps(1) preorder.simps(1) reflect.simps(1) rev.simps(1))
-  apply (metis Cons_eq_appendI postorder.simps(2) preorder.simps(2) reflect.simps(2) rev.simps(2) rev_append rotate1_def self_append_conv2)
+  apply (metis Cons_eq_appendI postorder.simps(2) preorder.simps(2) reflect.simps(2) rev.simps(2) rev_append self_append_conv2)
   done
 
 text {*
diff -r 6f79698f294d -r ba2bcae7aafd src/HOL/MetisExamples/Message.thy
--- a/src/HOL/MetisExamples/Message.thy	Thu Nov 22 14:51:34 2007 +0100
+++ b/src/HOL/MetisExamples/Message.thy	Fri Nov 23 17:37:56 2007 +0100
@@ -253,7 +253,7 @@
 
 ML{*ResAtp.problem_name := "Message__parts_cut"*}
 lemma parts_cut: "[|Y\<in> parts(insert X G);  X\<in> parts H|] ==> Y\<in> parts(G \<union> H)"
-by (metis Un_subset_iff Un_upper1 Un_upper2 insert_subset parts_Un parts_increasing parts_trans) 
+by (metis Un_subset_iff insert_subset parts_increasing parts_trans)