author nipkow Thu, 07 Jul 1994 19:47:34 +0200 changeset 453 d4e82b3a06c9 parent 452 395bbf6e55f9 child 454 0d19ab250cc9
added () around some of the ::
--- a/doc-src/Logics/Old_HOL.tex	Thu Jul 07 19:22:49 1994 +0200
+++ b/doc-src/Logics/Old_HOL.tex	Thu Jul 07 19:47:34 1994 +0200
@@ -225,9 +225,9 @@

\begin{figure}
\begin{ttbox}\makeatother
-\tdx{refl}           t = t::'a
+\tdx{refl}           t = (t::'a)
\tdx{subst}          [| s=t; P(s) |] ==> P(t::'a)
-\tdx{ext}            (!!x::'a. f(x)::'b = g(x)) ==> (\%x.f(x)) = (\%x.g(x))
+\tdx{ext}            (!!x::'a. (f(x)::'b) = g(x)) ==> (\%x.f(x)) = (\%x.g(x))
\tdx{impI}           (P ==> Q) ==> P-->Q
\tdx{mp}             [| P-->Q;  P |] ==> Q
\tdx{iff}            (P-->Q) --> (Q-->P) --> (P=Q)
@@ -240,7 +240,7 @@

\begin{figure}\hfuzz=4pt%suppress "Overfull \hbox" message
\begin{ttbox}\makeatother
-\tdx{True_def}   True  == ((\%x.x)=(\%x.x))
+\tdx{True_def}   True  == ((\%x::bool.x)=(\%x.x))
\tdx{All_def}    All   == (\%P. P = (\%x.True))
\tdx{Ex_def}     Ex    == (\%P. P(@x.P(x)))
\tdx{False_def}  False == (!P.P)
@@ -313,8 +313,8 @@
\tdx{trans}       [| r=s; s=t |] ==> r=t
\tdx{ssubst}      [| t=s; P(s) |] ==> P(t::'a)
\tdx{box_equals}  [| a=b;  a=c;  b=d |] ==> c=d
-\tdx{arg_cong}    s=t ==> f(s)=f(t)
-\tdx{fun_cong}    s::'a=>'b = t ==> s(x)=t(x)
+\tdx{arg_cong}    x=y ==> f(x)=f(y)
+\tdx{fun_cong}    f=g ==> f(x)=g(x)
\subcaption{Equality}

\tdx{TrueI}       True