# HG changeset patch
# User paulson
# Date 1235647289 0
# Node ID e1c714d33c5c922441b7db27eeff910b297376ca
# Parent  896fed07349e83750bcf3562fb9038fd31805854# Parent  dde11464969cd3b1b72a8db327f43cd6da55de5b
merged

diff -r 896fed07349e -r e1c714d33c5c doc-src/ZF/FOL.tex
--- 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"