803 \begin{matharray}{rcl} |
803 \begin{matharray}{rcl} |
804 \indexdef{HOL}{method}{iprover}\hypertarget{method.HOL.iprover}{\hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}}} & : & \isa{method} \\ |
804 \indexdef{HOL}{method}{iprover}\hypertarget{method.HOL.iprover}{\hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}}} & : & \isa{method} \\ |
805 \end{matharray} |
805 \end{matharray} |
806 |
806 |
807 \begin{rail} |
807 \begin{rail} |
808 'iprover' ('!' ?) ( rulemod * ) |
808 'iprover' ( rulemod * ) |
809 ; |
809 ; |
810 \end{rail} |
810 \end{rail} |
811 |
811 |
812 The \hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}} method performs intuitionistic proof |
812 The \hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}} method performs intuitionistic proof |
813 search, depending on specifically declared rules from the context, |
813 search, depending on specifically declared rules from the context, |
814 or given as explicit arguments. Chained facts are inserted into the |
814 or given as explicit arguments. Chained facts are inserted into the |
815 goal before commencing proof search; ``\hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' means to include the current \hyperlink{fact.prems}{\mbox{\isa{prems}}} as well. |
815 goal before commencing proof search. |
816 |
816 |
817 Rules need to be classified as \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}, |
817 Rules need to be classified as \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}, |
818 \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, or \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}; here the |
818 \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, or \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}; here the |
819 ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' indicator refers to ``safe'' rules, which may be |
819 ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' indicator refers to ``safe'' rules, which may be |
820 applied aggressively (without considering back-tracking later). |
820 applied aggressively (without considering back-tracking later). |
821 Rules declared with ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' are ignored in proof search (the |
821 Rules declared with ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' are ignored in proof search (the |