diff -r fac076f0c71c -r 9a23e4eb5eb3 src/HOL/UNITY/SubstAx.thy
--- a/src/HOL/UNITY/SubstAx.thy	Wed Aug 13 17:44:42 2003 +0200
+++ b/src/HOL/UNITY/SubstAx.thy	Fri Aug 15 13:07:01 2003 +0200
@@ -182,7 +182,7 @@
 apply (blast intro: EnsuresI LeadsTo_Basis Always_ConstrainsD [THEN Constrains_weaken] transient_strengthen)
 done
 
-text{*Set difference: maybe combine with leadsTo_weaken_L??
+text{*Set difference: maybe combine with @{text leadsTo_weaken_L}??
   This is the most useful form of the "disjunction" rule*}
 lemma LeadsTo_Diff:
      "[| F \<in> (A-B) LeadsTo C;  F \<in> (A \<inter> B) LeadsTo C |]