diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Library/AssocList.thy
--- a/src/HOL/Library/AssocList.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Library/AssocList.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -96,12 +96,12 @@
 (* ******************************************************************************** *)
 
 lemma delete_simps [simp]:
-"delete k [] = []"
-"delete k (p#ps) = (if fst p = k then delete k ps else p # delete k ps)"
+    "delete k [] = []"
+    "delete k (p#ps) = (if fst p = k then delete k ps else p # delete k ps)"
   by (simp_all add: delete_def)
 
 lemma delete_id[simp]: "k \<notin> fst ` set al \<Longrightarrow> delete k al = al"
-by(induct al, auto)
+  by (induct al) auto
 
 lemma delete_conv: "map_of (delete k al) k' = ((map_of al)(k := None)) k'"
   by (induct al) auto
@@ -112,9 +112,9 @@
 lemma delete_idem: "delete k (delete k al) = delete k al"
   by (induct al) auto
 
-lemma map_of_delete[simp]:
- "k' \<noteq> k \<Longrightarrow> map_of (delete k al) k' = map_of al k'"
-by(induct al, auto)
+lemma map_of_delete [simp]:
+    "k' \<noteq> k \<Longrightarrow> map_of (delete k al) k' = map_of al k'"
+  by (induct al) auto
 
 lemma delete_notin_dom: "k \<notin> fst ` set (delete k al)"
   by (induct al) auto
@@ -547,7 +547,7 @@
 
 lemma compose_conv: 
   shows "map_of (compose xs ys) k = (map_of ys \<circ>\<^sub>m map_of xs) k"
-proof (induct xs ys rule: compose_induct )
+proof (induct xs ys rule: compose_induct)
   case Nil thus ?case by simp
 next
   case (Cons x xs)
@@ -595,7 +595,7 @@
 using prems by (simp add: compose_conv)
 
 lemma dom_compose: "fst ` set (compose xs ys) \<subseteq> fst ` set xs"
-proof (induct xs ys rule: compose_induct )
+proof (induct xs ys rule: compose_induct)
   case Nil thus ?case by simp
 next
   case (Cons x xs)
@@ -799,12 +799,12 @@
  "map_of (update x y (restrict D al)) = map_of (update x y (restrict (D-{x}) al))"
   by (simp add: update_conv' restr_conv') (rule fun_upd_restrict)
 
-lemma upate_restr_conv[simp]:
+lemma upate_restr_conv [simp]:
  "x \<in> D \<Longrightarrow> 
  map_of (update x y (restrict D al)) = map_of (update x y (restrict (D-{x}) al))"
   by (simp add: update_conv' restr_conv')
 
-lemma restr_updates[simp]: "
+lemma restr_updates [simp]: "
  \<lbrakk> length xs = length ys; set xs \<subseteq> D \<rbrakk>
  \<Longrightarrow> map_of (restrict D (updates xs ys al)) = 
      map_of (updates xs ys (restrict (D - set xs) al))"