--- a/doc-src/IsarImplementation/style.sty Sun Nov 27 13:31:52 2011 +0100
+++ b/doc-src/IsarImplementation/style.sty Sun Nov 27 13:32:20 2011 +0100
@@ -64,7 +64,7 @@
\newcommand{\isasymTHEOREM}{\isakeyword{theorem}}
\newcommand{\isasymDEFINITION}{\isakeyword{definition}}
-\isabellestyle{itunderscore}
+\isabellestyle{literal}
\railtermfont{\isabellestyle{tt}}
\railnontermfont{\isabellestyle{itunderscore}}
--- a/doc-src/IsarRef/Thy/Generic.thy Sun Nov 27 13:31:52 2011 +0100
+++ b/doc-src/IsarRef/Thy/Generic.thy Sun Nov 27 13:32:20 2011 +0100
@@ -399,8 +399,8 @@
like @{text add}.
\medskip The @{text cong} modifiers add or delete Simplifier
- congruence rules (see also \cite{isabelle-ref}), the default is to
- add.
+ congruence rules (see also \secref{sec:simp-cong}), the default is
+ to add.
\medskip The @{text split} modifiers add or delete rules for the
Splitter (see also \cite{isabelle-ref}), the default is to add.
@@ -453,12 +453,11 @@
\begin{matharray}{rcl}
@{command_def "print_simpset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{attribute_def simp} & : & @{text attribute} \\
- @{attribute_def cong} & : & @{text attribute} \\
@{attribute_def split} & : & @{text attribute} \\
\end{matharray}
@{rail "
- (@@{attribute simp} | @@{attribute cong} | @@{attribute split}) (() | 'add' | 'del')
+ (@@{attribute simp} | @@{attribute split}) (() | 'add' | 'del')
"}
\begin{description}
@@ -469,14 +468,68 @@
\item @{attribute simp} declares simplification rules.
- \item @{attribute cong} declares congruence rules.
-
\item @{attribute split} declares case split rules.
\end{description}
*}
+subsection {* Congruence rules\label{sec:simp-cong} *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{attribute_def cong} & : & @{text attribute} \\
+ \end{matharray}
+
+ @{rail "
+ @@{attribute cong} (() | 'add' | 'del')
+ "}
+
+ \begin{description}
+
+ \item @{attribute cong} declares congruence rules to the Simplifier
+ context.
+
+ \end{description}
+
+ Congruence rules are equalities of the form @{text [display]
+ "\<dots> \<Longrightarrow> f ?x\<^sub>1 \<dots> ?x\<^sub>n = f ?y\<^sub>1 \<dots> ?y\<^sub>n"}
+
+ This controls the simplification of the arguments of @{text f}. For
+ example, some arguments can be simplified under additional
+ assumptions: @{text [display] "?P\<^sub>1 \<longleftrightarrow> ?Q\<^sub>1 \<Longrightarrow> (?Q\<^sub>1 \<Longrightarrow> ?P\<^sub>2 \<longleftrightarrow> ?Q\<^sub>2) \<Longrightarrow>
+ (?P\<^sub>1 \<longrightarrow> ?P\<^sub>2) \<longleftrightarrow> (?Q\<^sub>1 \<longrightarrow> ?Q\<^sub>2)"}
+
+ Given this rule, the simplifier assumes @{text "?Q\<^sub>1"} and extracts
+ rewrite rules from it when simplifying @{text "?P\<^sub>2"}. Such local
+ assumptions are effective for rewriting formulae such as @{text "x =
+ 0 \<longrightarrow> y + x = y"}.
+
+ %FIXME
+ %The local assumptions are also provided as theorems to the solver;
+ %see \secref{sec:simp-solver} below.
+
+ \medskip The following congruence rule for bounded quantifiers also
+ supplies contextual information --- about the bound variable:
+ @{text [display] "(?A = ?B) \<Longrightarrow> (\<And>x. x \<in> ?B \<Longrightarrow> ?P x \<longleftrightarrow> ?Q x) \<Longrightarrow>
+ (\<forall>x \<in> ?A. ?P x) \<longleftrightarrow> (\<forall>x \<in> ?B. ?Q x)"}
+
+ \medskip This congruence rule for conditional expressions can
+ supply contextual information for simplifying the arms:
+ @{text [display] "?p = ?q \<Longrightarrow> (?q \<Longrightarrow> ?a = ?c) \<Longrightarrow> (\<not> ?q \<Longrightarrow> ?b = ?d) \<Longrightarrow>
+ (if ?p then ?a else ?b) = (if ?q then ?c else ?d)"}
+
+ A congruence rule can also \emph{prevent} simplification of some
+ arguments. Here is an alternative congruence rule for conditional
+ expressions that conforms to non-strict functional evaluation:
+ @{text [display] "?p = ?q \<Longrightarrow> (if ?p then ?a else ?b) = (if ?q then ?a else ?b)"}
+
+ Only the first argument is simplified; the others remain unchanged.
+ This can make simplification much faster, but may require an extra
+ case split over the condition @{text "?q"} to prove the goal.
+*}
+
+
subsection {* Simplification procedures *}
text {* Simplification procedures are ML functions that produce proven
--- a/doc-src/IsarRef/Thy/document/Generic.tex Sun Nov 27 13:31:52 2011 +0100
+++ b/doc-src/IsarRef/Thy/document/Generic.tex Sun Nov 27 13:32:20 2011 +0100
@@ -653,8 +653,8 @@
like \isa{add}.
\medskip The \isa{cong} modifiers add or delete Simplifier
- congruence rules (see also \cite{isabelle-ref}), the default is to
- add.
+ congruence rules (see also \secref{sec:simp-cong}), the default is
+ to add.
\medskip The \isa{split} modifiers add or delete rules for the
Splitter (see also \cite{isabelle-ref}), the default is to add.
@@ -704,7 +704,6 @@
\begin{matharray}{rcl}
\indexdef{}{command}{print\_simpset}\hypertarget{command.print-simpset}{\hyperlink{command.print-simpset}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}simpset}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
\indexdef{}{attribute}{simp}\hypertarget{attribute.simp}{\hyperlink{attribute.simp}{\mbox{\isa{simp}}}} & : & \isa{attribute} \\
- \indexdef{}{attribute}{cong}\hypertarget{attribute.cong}{\hyperlink{attribute.cong}{\mbox{\isa{cong}}}} & : & \isa{attribute} \\
\indexdef{}{attribute}{split}\hypertarget{attribute.split}{\hyperlink{attribute.split}{\mbox{\isa{split}}}} & : & \isa{attribute} \\
\end{matharray}
@@ -713,8 +712,6 @@
\rail@bar
\rail@term{\hyperlink{attribute.simp}{\mbox{\isa{simp}}}}[]
\rail@nextbar{1}
-\rail@term{\hyperlink{attribute.cong}{\mbox{\isa{cong}}}}[]
-\rail@nextbar{2}
\rail@term{\hyperlink{attribute.split}{\mbox{\isa{split}}}}[]
\rail@endbar
\rail@bar
@@ -735,14 +732,87 @@
\item \hyperlink{attribute.simp}{\mbox{\isa{simp}}} declares simplification rules.
- \item \hyperlink{attribute.cong}{\mbox{\isa{cong}}} declares congruence rules.
-
\item \hyperlink{attribute.split}{\mbox{\isa{split}}} declares case split rules.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsubsection{Congruence rules\label{sec:simp-cong}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{attribute}{cong}\hypertarget{attribute.cong}{\hyperlink{attribute.cong}{\mbox{\isa{cong}}}} & : & \isa{attribute} \\
+ \end{matharray}
+
+ \begin{railoutput}
+\rail@begin{3}{}
+\rail@term{\hyperlink{attribute.cong}{\mbox{\isa{cong}}}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@term{\isa{add}}[]
+\rail@nextbar{2}
+\rail@term{\isa{del}}[]
+\rail@endbar
+\rail@end
+\end{railoutput}
+
+
+ \begin{description}
+
+ \item \hyperlink{attribute.cong}{\mbox{\isa{cong}}} declares congruence rules to the Simplifier
+ context.
+
+ \end{description}
+
+ Congruence rules are equalities of the form \begin{isabelle}%
+{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ f\ {\isaliteral{3F}{\isacharquery}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3F}{\isacharquery}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{3D}{\isacharequal}}\ f\ {\isaliteral{3F}{\isacharquery}}y\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3F}{\isacharquery}}y\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}%
+\end{isabelle}
+
+ This controls the simplification of the arguments of \isa{f}. For
+ example, some arguments can be simplified under additional
+ assumptions: \begin{isabelle}%
+{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}P\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ {\isaliteral{3F}{\isacharquery}}Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}P\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ {\isaliteral{3F}{\isacharquery}}Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\isanewline
+\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}P\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}P\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}%
+\end{isabelle}
+
+ Given this rule, the simplifier assumes \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} and extracts
+ rewrite rules from it when simplifying \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}P\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}}. Such local
+ assumptions are effective for rewriting formulae such as \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ y\ {\isaliteral{2B}{\isacharplus}}\ x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{22}{\isachardoublequote}}}.
+
+ %FIXME
+ %The local assumptions are also provided as theorems to the solver;
+ %see \secref{sec:simp-solver} below.
+
+ \medskip The following congruence rule for bounded quantifiers also
+ supplies contextual information --- about the bound variable:
+ \begin{isabelle}%
+{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}A\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{3F}{\isacharquery}}B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{3F}{\isacharquery}}B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}P\ x\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ {\isaliteral{3F}{\isacharquery}}Q\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\isanewline
+\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{3F}{\isacharquery}}A{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{3F}{\isacharquery}}B{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}Q\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}%
+\end{isabelle}
+
+ \medskip This congruence rule for conditional expressions can
+ supply contextual information for simplifying the arms:
+ \begin{isabelle}%
+{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}p\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{3F}{\isacharquery}}q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}a\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{3F}{\isacharquery}}c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{3F}{\isacharquery}}q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}b\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{3F}{\isacharquery}}d{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\isanewline
+\ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{3F}{\isacharquery}}p\ then\ {\isaliteral{3F}{\isacharquery}}a\ else\ {\isaliteral{3F}{\isacharquery}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{3F}{\isacharquery}}q\ then\ {\isaliteral{3F}{\isacharquery}}c\ else\ {\isaliteral{3F}{\isacharquery}}d{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}%
+\end{isabelle}
+
+ A congruence rule can also \emph{prevent} simplification of some
+ arguments. Here is an alternative congruence rule for conditional
+ expressions that conforms to non-strict functional evaluation:
+ \begin{isabelle}%
+{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}p\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{3F}{\isacharquery}}q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{3F}{\isacharquery}}p\ then\ {\isaliteral{3F}{\isacharquery}}a\ else\ {\isaliteral{3F}{\isacharquery}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{3F}{\isacharquery}}q\ then\ {\isaliteral{3F}{\isacharquery}}a\ else\ {\isaliteral{3F}{\isacharquery}}b{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}%
+\end{isabelle}
+
+ Only the first argument is simplified; the others remain unchanged.
+ This can make simplification much faster, but may require an extra
+ case split over the condition \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}q{\isaliteral{22}{\isachardoublequote}}} to prove the goal.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsubsection{Simplification procedures%
}
\isamarkuptrue%
--- a/doc-src/IsarRef/style.sty Sun Nov 27 13:31:52 2011 +0100
+++ b/doc-src/IsarRef/style.sty Sun Nov 27 13:32:20 2011 +0100
@@ -36,8 +36,8 @@
\parindent 0pt\parskip 0.5ex
-\isabellestyle{itunderscore}
+\isabellestyle{literal}
\railtermfont{\isabellestyle{tt}}
-\railnontermfont{\isabellestyle{itunderscore}}
-\railnamefont{\isabellestyle{itunderscore}}
+\railnontermfont{\isabellestyle{literal}}
+\railnamefont{\isabellestyle{literal}}
--- a/doc-src/Ref/simplifier.tex Sun Nov 27 13:31:52 2011 +0100
+++ b/doc-src/Ref/simplifier.tex Sun Nov 27 13:32:20 2011 +0100
@@ -336,75 +336,6 @@
\index{rewrite rules|)}
-\subsection{*Congruence rules}\index{congruence rules}\label{sec:simp-congs}
-\begin{ttbox}
-addcongs : simpset * thm list -> simpset \hfill{\bf infix 4}
-delcongs : simpset * thm list -> simpset \hfill{\bf infix 4}
-addeqcongs : simpset * thm list -> simpset \hfill{\bf infix 4}
-deleqcongs : simpset * thm list -> simpset \hfill{\bf infix 4}
-\end{ttbox}
-
-Congruence rules are meta-equalities of the form
-\[ \dots \Imp
- f(\Var{x@1},\ldots,\Var{x@n}) \equiv f(\Var{y@1},\ldots,\Var{y@n}).
-\]
-This governs the simplification of the arguments of~$f$. For
-example, some arguments can be simplified under additional assumptions:
-\[ \List{\Var{P@1} \bimp \Var{Q@1};\; \Var{Q@1} \Imp \Var{P@2} \bimp \Var{Q@2}}
- \Imp (\Var{P@1} \imp \Var{P@2}) \equiv (\Var{Q@1} \imp \Var{Q@2})
-\]
-Given this rule, the simplifier assumes $Q@1$ and extracts rewrite
-rules from it when simplifying~$P@2$. Such local assumptions are
-effective for rewriting formulae such as $x=0\imp y+x=y$. The local
-assumptions are also provided as theorems to the solver; see
-{\S}~\ref{sec:simp-solver} below.
-
-\begin{ttdescription}
-
-\item[$ss$ \ttindexbold{addcongs} $thms$] adds congruence rules to the
- simpset $ss$. These are derived from $thms$ in an appropriate way,
- depending on the underlying object-logic.
-
-\item[$ss$ \ttindexbold{delcongs} $thms$] deletes congruence rules
- derived from $thms$.
-
-\item[$ss$ \ttindexbold{addeqcongs} $thms$] adds congruence rules in
- their internal form (conclusions using meta-equality) to simpset
- $ss$. This is the basic mechanism that \texttt{addcongs} is built
- on. It should be rarely used directly.
-
-\item[$ss$ \ttindexbold{deleqcongs} $thms$] deletes congruence rules
- in internal form from simpset $ss$.
-
-\end{ttdescription}
-
-\medskip
-
-Here are some more examples. The congruence rule for bounded
-quantifiers also supplies contextual information, this time about the
-bound variable:
-\begin{eqnarray*}
- &&\List{\Var{A}=\Var{B};\;
- \Forall x. x\in \Var{B} \Imp \Var{P}(x) = \Var{Q}(x)} \Imp{} \\
- &&\qquad\qquad
- (\forall x\in \Var{A}.\Var{P}(x)) = (\forall x\in \Var{B}.\Var{Q}(x))
-\end{eqnarray*}
-The congruence rule for conditional expressions can supply contextual
-information for simplifying the arms:
-\[ \List{\Var{p}=\Var{q};~ \Var{q} \Imp \Var{a}=\Var{c};~
- \neg\Var{q} \Imp \Var{b}=\Var{d}} \Imp
- if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{c},\Var{d})
-\]
-A congruence rule can also {\em prevent\/} simplification of some arguments.
-Here is an alternative congruence rule for conditional expressions:
-\[ \Var{p}=\Var{q} \Imp
- if(\Var{p},\Var{a},\Var{b}) \equiv if(\Var{q},\Var{a},\Var{b})
-\]
-Only the first argument is simplified; the others remain unchanged.
-This can make simplification much faster, but may require an extra case split
-to prove the goal.
-
-
\subsection{*The subgoaler}\label{sec:simp-subgoaler}
\begin{ttbox}
setsubgoaler :
--- a/lib/texinputs/isabelle.sty Sun Nov 27 13:31:52 2011 +0100
+++ b/lib/texinputs/isabelle.sty Sun Nov 27 13:32:20 2011 +0100
@@ -194,10 +194,12 @@
\def\isacharverbatimclose{\isamath{\rangle\!\rangle}}%
}
-\newcommand{\isabellestyleitunderscore}{%
+\newcommand{\isabellestyleliteral}{%
\isabellestyleit%
\def\isacharunderscore{\_}%
\def\isacharunderscorekeyword{\_}%
+\chardef\isacharbackquoteopen=`\`%
+\chardef\isacharbackquoteclose=`\`%
}
\newcommand{\isabellestylesl}{%