doc-src/IsarRef/Thy/document/Spec.tex
changeset 29754 2203ef9b55ce
parent 29746 533c27b43ee1
child 30121 5c7bcb296600
equal deleted inserted replaced
29753:a9fc00f1b8f0 29754:2203ef9b55ce
  1194   specification of axioms!  Invoking the oracle only works within the
  1194   specification of axioms!  Invoking the oracle only works within the
  1195   scope of the resulting theory.
  1195   scope of the resulting theory.
  1196 
  1196 
  1197   \end{description}
  1197   \end{description}
  1198 
  1198 
  1199   See \hyperlink{file.~~/src/FOL/ex/IffOracle.thy}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}FOL{\isacharslash}ex{\isacharslash}IffOracle{\isachardot}thy}}}} for a worked example of
  1199   See \hyperlink{file.~~/src/FOL/ex/Iff-Oracle.thy}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}FOL{\isacharslash}ex{\isacharslash}Iff{\isacharunderscore}Oracle{\isachardot}thy}}}} for a worked example of
  1200   defining a new primitive rule as oracle, and turning it into a proof
  1200   defining a new primitive rule as oracle, and turning it into a proof
  1201   method.%
  1201   method.%
  1202 \end{isamarkuptext}%
  1202 \end{isamarkuptext}%
  1203 \isamarkuptrue%
  1203 \isamarkuptrue%
  1204 %
  1204 %