# HG changeset patch # User huffman # Date 1235659146 28800 # Node ID b094999e1d334f6b8ae1503aeaed34fa98b1e879 # Parent 32effb2a8168aedfdabf8ac652cbad1fdb3399a0# Parent e1c714d33c5c922441b7db27eeff910b297376ca merged diff -r 32effb2a8168 -r b094999e1d33 doc-src/ZF/FOL.tex --- a/doc-src/ZF/FOL.tex Thu Feb 26 06:33:48 2009 -0800 +++ b/doc-src/ZF/FOL.tex Thu Feb 26 06:39:06 2009 -0800 @@ -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"