1.1 --- a/doc-src/ZF/FOL.tex	Wed Feb 18 11:18:01 2009 +0000
     1.2 +++ b/doc-src/ZF/FOL.tex	Thu Feb 26 11:18:40 2009 +0000
     1.3 @@ -1,4 +1,4 @@
     1.4 -%% $Id$
     1.5 +%!TEX root = logics-ZF.tex
     1.6  \chapter{First-Order Logic}
     1.7  \index{first-order logic|(}
     1.8  
     1.9 @@ -360,7 +360,8 @@
    1.10  logic by designating \isa{IFOL} rather than \isa{FOL} as the parent
    1.11  theory:
    1.12  \begin{isabelle}
    1.13 -\isacommand{theory}\ IFOL\_examples\ =\ IFOL:
    1.14 +\isacommand{theory}\ IFOL\_examples\ \isacommand{imports}\ IFOL\isanewline
    1.15 +\isacommand{begin}
    1.16  \end{isabelle}
    1.17  The proof begins by entering the goal, then applying the rule $({\imp}I)$.
    1.18  \begin{isabelle}
    1.19 @@ -441,7 +442,7 @@
    1.20  \ 1.\ (\isasymexists y.\ \isasymforall x.\ Q(x,\ y))\
    1.21  \isasymlongrightarrow \ (\isasymforall x.\ \isasymexists y.\ Q(x,\ y))
    1.22  \isanewline
    1.23 -\isacommand{by} (tactic {*IntPr.fast_tac 1*})\isanewline
    1.24 +\isacommand{by} (tactic \ttlbrace*IntPr.fast_tac 1*\ttrbrace)\isanewline
    1.25  No\ subgoals!
    1.26  \end{isabelle}
    1.27  
    1.28 @@ -529,7 +530,8 @@
    1.29  $\all{x}P(x)$ is true.  Either way the theorem holds.  First, we must
    1.30  work in a theory based on classical logic, the theory \isa{FOL}:
    1.31  \begin{isabelle}
    1.32 -\isacommand{theory}\ FOL\_examples\ =\ FOL:
    1.33 +\isacommand{theory}\ FOL\_examples\ \isacommand{imports}\ FOL\isanewline
    1.34 +\isacommand{begin}
    1.35  \end{isabelle}
    1.36  
    1.37  The formal proof does not conform in any obvious way to the sketch given
    1.38 @@ -631,7 +633,8 @@
    1.39  $if::[o,o,o]\To o$.  The axiom \tdx{if_def} asserts the
    1.40  equation~$(if)$.
    1.41  \begin{isabelle}
    1.42 -\isacommand{theory}\ If\ =\ FOL:\isanewline
    1.43 +\isacommand{theory}\ If\ \isacommand{imports}\ FOL\isanewline
    1.44 +\isacommand{begin}\isanewline
    1.45  \isacommand{constdefs}\isanewline
    1.46  \ \ if\ ::\ "[o,o,o]=>o"\isanewline
    1.47  \ \ \ "if(P,Q,R)\ ==\ P\&Q\ |\ \isachartilde P\&R"