proper LaTeX;

--- a/src/HOL/HOL.thy	Sun Jul 19 21:16:39 2015 +0200
+++ b/src/HOL/HOL.thy	Mon Jul 20 11:40:43 2015 +0200
@@ -1330,7 +1330,7 @@
 
 ML \<open>val HOL_ss = simpset_of @{context}\<close>
 
-text \<open>Simplifies x assuming c and y assuming \<not> c\<close>
+text \<open>Simplifies @{term x} assuming @{prop c} and @{term y} assuming @{prop "\<not> c"}\<close>
 lemma if_cong:
   assumes "b = c"
       and "c \<Longrightarrow> x = u"