equal
deleted
inserted
replaced
678 to be proven by forward chaining the current facts. Note that $\HENCENAME$ |
678 to be proven by forward chaining the current facts. Note that $\HENCENAME$ |
679 is also equivalent to $\FROM{this}~\HAVENAME$. |
679 is also equivalent to $\FROM{this}~\HAVENAME$. |
680 \item [$\THUSNAME$] abbreviates $\THEN~\SHOWNAME$. Note that $\THUSNAME$ is |
680 \item [$\THUSNAME$] abbreviates $\THEN~\SHOWNAME$. Note that $\THUSNAME$ is |
681 also equivalent to $\FROM{this}~\SHOWNAME$. |
681 also equivalent to $\FROM{this}~\SHOWNAME$. |
682 \end{descr} |
682 \end{descr} |
|
683 |
|
684 Note that any goal statement causes some term abbreviations (such as |
|
685 $\Var{thesis}$, $\dots$) to be bound automatically, see also |
|
686 \S\ref{sec:term-abbrev}. Furthermore, the local context of a (non-atomic) |
|
687 goal is provided via the case name $antecedent$\indexisarcase{antecedent}, see |
|
688 also \S\ref{sec:cases}. |
683 |
689 |
684 |
690 |
685 \subsection{Initial and terminal proof steps}\label{sec:proof-steps} |
691 \subsection{Initial and terminal proof steps}\label{sec:proof-steps} |
686 |
692 |
687 \indexisarcmd{proof}\indexisarcmd{qed}\indexisarcmd{by} |
693 \indexisarcmd{proof}\indexisarcmd{qed}\indexisarcmd{by} |