equal
deleted
inserted
replaced
433 plain natural deduction rules for the primary connectives \isa{{\isasymAnd}} and \isa{{\isasymLongrightarrow}} of the framework. There is also a builtin |
433 plain natural deduction rules for the primary connectives \isa{{\isasymAnd}} and \isa{{\isasymLongrightarrow}} of the framework. There is also a builtin |
434 notion of equality/equivalence \isa{{\isasymequiv}}.% |
434 notion of equality/equivalence \isa{{\isasymequiv}}.% |
435 \end{isamarkuptext}% |
435 \end{isamarkuptext}% |
436 \isamarkuptrue% |
436 \isamarkuptrue% |
437 % |
437 % |
438 \isamarkupsubsection{Primitive connectives and rules% |
438 \isamarkupsubsection{Primitive connectives and rules \label{sec:prim_rules}% |
439 } |
439 } |
440 \isamarkuptrue% |
440 \isamarkuptrue% |
441 % |
441 % |
442 \begin{isamarkuptext}% |
442 \begin{isamarkuptext}% |
443 The theory \isa{Pure} contains constant declarations for the |
443 The theory \isa{Pure} contains constant declarations for the |