author paulson Thu, 26 Feb 2009 11:18:40 +0000 changeset 30099 dde11464969c parent 29960 9d5c6f376768 child 30100 e1c714d33c5c
Updated the theory syntax. Corrected an error in a command.
 doc-src/ZF/FOL.tex file | annotate | diff | comparison | revisions
--- a/doc-src/ZF/FOL.tex	Wed Feb 18 11:18:01 2009 +0000
+++ b/doc-src/ZF/FOL.tex	Thu Feb 26 11:18:40 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"