equal
deleted
inserted
replaced
802 \item [$\IS{\vec p}$] resembles $\LETNAME$, but matches $\vec p$ against the |
802 \item [$\IS{\vec p}$] resembles $\LETNAME$, but matches $\vec p$ against the |
803 preceding statement. Also note that $\ISNAME$ is not a separate command, |
803 preceding statement. Also note that $\ISNAME$ is not a separate command, |
804 but part of others (such as $\ASSUMENAME$, $\HAVENAME$ etc.). |
804 but part of others (such as $\ASSUMENAME$, $\HAVENAME$ etc.). |
805 \end{descr} |
805 \end{descr} |
806 |
806 |
807 A few \emph{automatic} term abbreviations\index{automatic abbreviation} for |
807 A few \emph{automatic} term abbreviations\index{term abbreviations} for goals |
808 goals and facts are available as well. For any open goal, |
808 and facts are available as well. For any open goal, |
809 $\Var{thesis_prop}$\indexisarvar{thesis-prop} refers to the full proposition |
809 $\Var{thesis_prop}$\indexisarvar{thesis-prop} refers to the full proposition |
810 (which may be a rule), $\Var{thesis_concl}$\indexisarvar{thesis-concl} to its |
810 (which may be a rule), $\Var{thesis_concl}$\indexisarvar{thesis-concl} to its |
811 (atomic) conclusion, and $\Var{thesis}$\indexisarvar{thesis} to its |
811 (atomic) conclusion, and $\Var{thesis}$\indexisarvar{thesis} to its |
812 object-logical statement. The latter two abstract over any meta-level |
812 object-logical statement. The latter two abstract over any meta-level |
813 parameters. |
813 parameters. |