# HG changeset patch # User paulson # Date 1235647120 0 # Node ID dde11464969cd3b1b72a8db327f43cd6da55de5b # Parent 9d5c6f376768cd377f011507e2caa560a8b7b4bc Updated the theory syntax. Corrected an error in a command. diff -r 9d5c6f376768 -r dde11464969c doc-src/ZF/FOL.tex --- 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"