author | wenzelm |
Mon, 20 Jul 2015 11:40:43 +0200 | |
changeset 60761 | a443b08281e2 |
parent 60760 | 3444e0bf9261 |
child 60762 | bf0c76ccee8d |
src/HOL/HOL.thy | file | annotate | diff | comparison | revisions |
--- 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"