# HG changeset patch
# User wenzelm
# Date 1437385243 -7200
# Node ID a443b08281e221082864b544d05c1bdc1e4f7ff3
# Parent  3444e0bf92615ff7721c3431915bb00986a9afb3
proper LaTeX;

diff -r 3444e0bf9261 -r a443b08281e2 src/HOL/HOL.thy
--- 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"