author paulson Thu, 26 Feb 2009 11:21:29 +0000 changeset 30100 e1c714d33c5c parent 30098 896fed07349e (current diff) parent 30099 dde11464969c (diff) child 30101 5c6efec476ae child 30104 b094999e1d33
merged
--- a/doc-src/ZF/FOL.tex	Wed Feb 25 11:30:46 2009 -0800
+++ b/doc-src/ZF/FOL.tex	Thu Feb 26 11:21:29 2009 +0000
@@ -1,4 +1,4 @@
-%% $Id$
+%!TEX root = logics-ZF.tex
\chapter{First-Order Logic}
\index{first-order logic|(}

@@ -360,7 +360,8 @@
logic by designating \isa{IFOL} rather than \isa{FOL} as the parent
theory:
\begin{isabelle}
-\isacommand{theory}\ IFOL\_examples\ =\ IFOL:
+\isacommand{theory}\ IFOL\_examples\ \isacommand{imports}\ IFOL\isanewline
+\isacommand{begin}
\end{isabelle}
The proof begins by entering the goal, then applying the rule $({\imp}I)$.
\begin{isabelle}
@@ -441,7 +442,7 @@
\ 1.\ (\isasymexists y.\ \isasymforall x.\ Q(x,\ y))\
\isasymlongrightarrow \ (\isasymforall x.\ \isasymexists y.\ Q(x,\ y))
\isanewline
-\isacommand{by} (tactic {*IntPr.fast_tac 1*})\isanewline
+\isacommand{by} (tactic \ttlbrace*IntPr.fast_tac 1*\ttrbrace)\isanewline
No\ subgoals!
\end{isabelle}

@@ -529,7 +530,8 @@
$\all{x}P(x)$ is true.  Either way the theorem holds.  First, we must
work in a theory based on classical logic, the theory \isa{FOL}:
\begin{isabelle}
-\isacommand{theory}\ FOL\_examples\ =\ FOL:
+\isacommand{theory}\ FOL\_examples\ \isacommand{imports}\ FOL\isanewline
+\isacommand{begin}
\end{isabelle}

The formal proof does not conform in any obvious way to the sketch given
@@ -631,7 +633,8 @@
$if::[o,o,o]\To o$.  The axiom \tdx{if_def} asserts the
equation~$(if)$.
\begin{isabelle}
-\isacommand{theory}\ If\ =\ FOL:\isanewline
+\isacommand{theory}\ If\ \isacommand{imports}\ FOL\isanewline
+\isacommand{begin}\isanewline
\isacommand{constdefs}\isanewline
\ \ if\ ::\ "[o,o,o]=>o"\isanewline
\ \ \ "if(P,Q,R)\ ==\ P\&Q\ |\ \isachartilde P\&R"