src/Doc/Tutorial/Sets/Functions.thy
changeset 58860 fee7cfa69c50
parent 56154 f0a927235162
child 67406 23307fd33906
     1.1 --- a/src/Doc/Tutorial/Sets/Functions.thy	Sat Nov 01 11:40:55 2014 +0100
     1.2 +++ b/src/Doc/Tutorial/Sets/Functions.thy	Sat Nov 01 14:20:38 2014 +0100
     1.3 @@ -73,7 +73,7 @@
     1.4  \rulename{fun_eq_iff}
     1.5  *}
     1.6  
     1.7 -lemma "inj f \<Longrightarrow> (f o g = f o h) = (g = h)";
     1.8 +lemma "inj f \<Longrightarrow> (f o g = f o h) = (g = h)"
     1.9    apply (simp add: fun_eq_iff inj_on_def)
    1.10    apply (auto)
    1.11    done