diff -r c96e007b512f -r da5e4b8317c7 Quot/QuotList.thy
--- a/Quot/QuotList.thy	Tue Jan 26 01:42:46 2010 +0100
+++ b/Quot/QuotList.thy	Tue Jan 26 10:53:44 2010 +0100
@@ -1,4 +1,4 @@
-theory QuotList
+ theory QuotList
 imports QuotMain List
 begin
 
@@ -17,13 +17,13 @@
 text {* should probably be in Sum_Type.thy *}
 lemma split_list_all: 
   shows "(\<forall>x. P x) \<longleftrightarrow> P [] \<and> (\<forall>x xs. P (x#xs))"
-apply(auto)
-apply(case_tac x)
-apply(simp_all)
-done
+  apply(auto)
+  apply(case_tac x)
+  apply(simp_all)
+  done
 
-lemma map_id[id_simps]: "map id \<equiv> id"
-  apply(rule eq_reflection)
+lemma map_id[id_simps]: 
+  shows "map id = id"
   apply(simp add: expand_fun_eq)
   apply(rule allI)
   apply(induct_tac x)
@@ -112,8 +112,8 @@
 
 lemma nil_prs[quot_preserve]:
   assumes q: "Quotient R Abs Rep"
-  shows "map Abs [] \<equiv> []"
-  by (simp)
+  shows "map Abs [] = []"
+  by simp
 
 lemma nil_rsp[quot_respect]:
   assumes q: "Quotient R Abs Rep"
@@ -215,8 +215,7 @@
   done
 
 lemma list_rel_eq[id_simps]:
-  shows "list_rel (op =) \<equiv> (op =)"
-  apply(rule eq_reflection)
+  shows "(list_rel (op =)) = (op =)"
   unfolding expand_fun_eq
   apply(rule allI)+
   apply(induct_tac x xa rule: list_induct2')