Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
doc-src/Logics/Old_HOL.tex
changeset 841 14b96e3bd4ab
parent 705 9fb068497df4
child 861 28a593f4b600 
--- a/doc-src/Logics/Old_HOL.tex	Mon Jan 02 12:14:26 1995 +0100
+++ b/doc-src/Logics/Old_HOL.tex	Mon Jan 02 12:16:12 1995 +0100
@@ -604,7 +604,7 @@
 \tdx{mem_Collect_eq}    (a : \{x.P(x)\}) = P(a)
 \tdx{Collect_mem_eq}    \{x.x:A\} = A
 
-\tdx{empty_def}         \{\}          == \{x.x=False\}
+\tdx{empty_def}         \{\}          == \{x.False\}
 \tdx{insert_def}        insert(a,B) == \{x.x=a\} Un B
 \tdx{Ball_def}          Ball(A,P)   == ! x. x:A --> P(x)
 \tdx{Bex_def}           Bex(A,P)    == ? x. x:A & P(x)
isabelle