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)