src/Doc/Tutorial/Sets/Functions.thy

--- a/src/Doc/Tutorial/Sets/Functions.thy	Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Sets/Functions.thy	Sat Nov 01 14:20:38 2014 +0100
@@ -73,7 +73,7 @@
 \rulename{fun_eq_iff}
 *}
 
-lemma "inj f \<Longrightarrow> (f o g = f o h) = (g = h)";
+lemma "inj f \<Longrightarrow> (f o g = f o h) = (g = h)"
   apply (simp add: fun_eq_iff inj_on_def)
   apply (auto)
   done