equal
deleted
inserted
replaced
669 \begin{ttbox} |
669 \begin{ttbox} |
670 Delrules : thm list -> unit |
670 Delrules : thm list -> unit |
671 \end{ttbox} |
671 \end{ttbox} |
672 deletes rules from the current claset. |
672 deletes rules from the current claset. |
673 |
673 |
674 \medskip A few further functions are available as uppercase versions only: |
|
675 \begin{ttbox} |
|
676 AddXIs, AddXEs, AddXDs: thm list -> unit |
|
677 \end{ttbox} |
|
678 \indexbold{*AddXIs} \indexbold{*AddXEs} \indexbold{*AddXDs} augment the |
|
679 current claset by \emph{extra} introduction, elimination, or destruct rules. |
|
680 These provide additional hints for the basic non-automated proof methods of |
|
681 Isabelle/Isar \cite{isabelle-isar-ref}. The corresponding Isar attributes are |
|
682 ``$intro?$'', ``$elim?$'', and ``$dest?$''. Note that these extra rules do |
|
683 not have any effect on classic Isabelle tactics. |
|
684 |
|
685 |
674 |
686 \subsection{Accessing the current claset} |
675 \subsection{Accessing the current claset} |
687 \label{sec:access-current-claset} |
676 \label{sec:access-current-claset} |
688 |
677 |
689 the functions to access the current claset are analogous to the functions |
678 the functions to access the current claset are analogous to the functions |