less digestible
authorhaftmann
Mon Jul 20 15:24:15 2009 +0200 (2009-07-20)
changeset 3208290d03908b3d7
parent 32081 1b7a901e2edc
child 32083 b916fb3f9136
less digestible
src/HOL/Set.thy
     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"