# HG changeset patch
# User haftmann
# Date 1248096255 -7200
# Node ID 90d03908b3d7f58f598ebce6ca1d319c395e61dd
# Parent  1b7a901e2edc519f922d807f4a04693eafb35d71
less digestible

diff -r 1b7a901e2edc -r 90d03908b3d7 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Jul 20 11:47:17 2009 +0200
+++ b/src/HOL/Set.thy	Mon Jul 20 15:24:15 2009 +0200
@@ -589,7 +589,7 @@
   by blast
 
 lemma equals0D: "A = {} ==> a \<notin> A"
-    -- {* Use for reasoning about disjointness: @{prop "A Int B = {}"} *}
+    -- {* Use for reasoning about disjointness: @{text "A Int B = {}"} *}
   by blast
 
 lemma ball_empty [simp]: "Ball {} P = True"