doc-src/IsarImplementation/Thy/document/logic.tex
changeset 20929 cd2a6d00ec47
parent 20547 796ae7fa1049
child 21324 a5089fc012b5
equal deleted 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