src/HOL/Set.thy
changeset 32082 90d03908b3d7
parent 32081 1b7a901e2edc
child 32115 8f10fb3bb46e
     1.1 --- a/src/HOL/Set.thy	Mon Jul 20 11:47:17 2009 +0200
     1.2 +++ b/src/HOL/Set.thy	Mon Jul 20 15:24:15 2009 +0200
     1.3 @@ -589,7 +589,7 @@
     1.4    by blast
     1.5  
     1.6  lemma equals0D: "A = {} ==> a \<notin> A"
     1.7 -    -- {* Use for reasoning about disjointness: @{prop "A Int B = {}"} *}
     1.8 +    -- {* Use for reasoning about disjointness: @{text "A Int B = {}"} *}
     1.9    by blast
    1.10  
    1.11  lemma ball_empty [simp]: "Ball {} P = True"