doc-src/IsarImplementation/Thy/document/logic.tex
changeset 26873 691f35f855cd
parent 26854 9b4aec46ad78
child 28086 db584d1d2af4
equal deleted inserted replaced
26872:336dfd860744 26873:691f35f855cd
   436   plain natural deduction rules for the primary connectives \isa{{\isasymAnd}} and \isa{{\isasymLongrightarrow}} of the framework.  There is also a builtin
   436   plain natural deduction rules for the primary connectives \isa{{\isasymAnd}} and \isa{{\isasymLongrightarrow}} of the framework.  There is also a builtin
   437   notion of equality/equivalence \isa{{\isasymequiv}}.%
   437   notion of equality/equivalence \isa{{\isasymequiv}}.%
   438 \end{isamarkuptext}%
   438 \end{isamarkuptext}%
   439 \isamarkuptrue%
   439 \isamarkuptrue%
   440 %
   440 %
   441 \isamarkupsubsection{Primitive connectives and rules \label{sec:prim_rules}%
   441 \isamarkupsubsection{Primitive connectives and rules \label{sec:prim-rules}%
   442 }
   442 }
   443 \isamarkuptrue%
   443 \isamarkuptrue%
   444 %
   444 %
   445 \begin{isamarkuptext}%
   445 \begin{isamarkuptext}%
   446 The theory \isa{Pure} contains constant declarations for the
   446 The theory \isa{Pure} contains constant declarations for the