--- a/Myhill_2.thy	Tue Mar 06 11:30:45 2012 +0000
+++ b/Myhill_2.thy	Fri Apr 13 13:12:43 2012 +0000
@@ -1,3 +1,4 @@
+(* Author: Xingyuan Zhang, Chunhan Wu, Christian Urban *)
 theory Myhill_2
   imports Myhill_1 "~~/src/HOL/Library/List_Prefix"
 begin
@@ -56,7 +57,7 @@
         by (simp) (blast)
       with X_in Y_in 
       have "X = Y"
-	unfolding quotient_def tag_eq_def by auto
+        unfolding quotient_def tag_eq_def by auto
     } 
     then show "inj_on ?f ?A" unfolding inj_on_def by auto
   qed
@@ -324,7 +325,7 @@
   "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists> max \<in> A. \<forall> a \<in> A. length a \<le> length max"
 apply(induct rule:finite.induct)
 apply(simp)
-by (metis (full_types) all_not_in_conv insert_iff linorder_linear order_trans)
+by (metis (hide_lams, no_types) all_not_in_conv insert_iff linorder_le_cases order_trans)
 
 lemma finite_strict_prefix_set: 
   shows "finite {xa. xa < (x::'a list)}"