doc-src/IsarImplementation/Thy/document/logic.tex
 changeset 20929 cd2a6d00ec47 parent 20547 796ae7fa1049 child 21324 a5089fc012b5
equal inserted replaced
20928:74910a189f1d 20929:cd2a6d00ec47
   773 %
   773 %
   774 \isamarkupsection{Rules \label{sec:rules}%
   774 \isamarkupsection{Rules \label{sec:rules}%
   775 }
   775 }
   776 \isamarkuptrue%
   776 \isamarkuptrue%
   777 %
   777 %

   778 \isadelimFIXME

   779 %

   780 \endisadelimFIXME

   781 %

   782 \isatagFIXME

   783 %
   778 \begin{isamarkuptext}%
   784 \begin{isamarkuptext}%
   779 FIXME
   785 FIXME
   780
   786
   781   A \emph{rule} is any Pure theorem in HHF normal form; there is a
   787   A \emph{rule} is any Pure theorem in HHF normal form; there is a
   782   separate calculus for rule composition, which is modeled after
   788   separate calculus for rule composition, which is modeled after
   855
   861
   856   FIXME \isa{elim{\isacharunderscore}resolution}, \isa{dest{\isacharunderscore}resolution}%
   862   FIXME \isa{elim{\isacharunderscore}resolution}, \isa{dest{\isacharunderscore}resolution}%
   857 \end{isamarkuptext}%
   863 \end{isamarkuptext}%
   858 \isamarkuptrue%
   864 \isamarkuptrue%
   859 %
   865 %

   866 \endisatagFIXME

   867 {\isafoldFIXME}%

   868 %

   869 \isadelimFIXME

   870 %

   871 \endisadelimFIXME

   872 %
   860 \isadelimtheory
   873 \isadelimtheory
   861 %
   874 %
   862 \endisadelimtheory
   875 \endisadelimtheory
   863 %
   876 %
   864 \isatagtheory
   877 \isatagtheory