author | webertj |
Thu, 23 Nov 2006 13:32:19 +0100 | |
changeset 21486 | b1fdc0513812 |
parent 21485 | 44f616cc8985 |
child 21487 | 45f9163d79e7 |
src/HOL/HOL.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/HOL.thy Thu Nov 23 11:39:11 2006 +0100 +++ b/src/HOL/HOL.thy Thu Nov 23 13:32:19 2006 +0100 @@ -259,7 +259,7 @@ shows "A = B" by (unfold meq) (rule refl) -text {* Useful with eresolve\_tac for proving equalties from known equalities. *} +text {* Useful with eresolve\_tac for proving equalities from known equalities. *} (* a = b | | c = d *)