Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
less digestible
authorhaftmann
Mon, 20 Jul 2009 15:24:15 +0200
changeset 32082 90d03908b3d7
parent 32081 1b7a901e2edc
child 32083 b916fb3f9136
less digestible
src/HOL/Set.thy file | annotate | diff | comparison | revisions 
--- 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"
isabelle