src/HOL/Fun.thy

   "a o b = c o d \<Longrightarrow> a (b v) = c (d v)"
   by (simp add: fun_eq_iff)
 
 lemma comp_eq_elim:
   "a o b = c o d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
-  by (simp add: fun_eq_iff) 
+  by (simp add: fun_eq_iff)
 
 lemma comp_eq_dest_lhs: "a o b = c \<Longrightarrow> a (b v) = c v"
   by clarsimp
 
 lemma comp_eq_id_dest: "a o b = id o c \<Longrightarrow> a (b v) = c v"

   have "?X \<in> Pow A" unfolding Pow_def by auto
   with * obtain x where "x \<in> A \<and> f x = ?X" by blast
   thus False by best
 qed
 
-subsection \<open>Setup\<close> 
+subsection \<open>Setup\<close>
 
 subsubsection \<open>Proof tools\<close>
 
 text \<open>simplifies terms of the form
   f(...,x:=y,...,x:=z,...) to f(...,x:=z,...)\<close>