# HG changeset patch # User nipkow # Date 1322397140 -3600 # Node ID 003a01272d280156e7f72915508f520bd7cbfb5c # Parent 02afa20cf397040c0a3b01d19147b9aafb1f3dae# Parent a49f9428aba45588639666605c6753d0c23dcae4 merged diff -r a49f9428aba4 -r 003a01272d28 doc-src/IsarImplementation/style.sty --- 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}} diff -r a49f9428aba4 -r 003a01272d28 doc-src/IsarRef/Thy/Generic.thy --- 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 \"} \\ @{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] + "\ \ f ?x\<^sub>1 \ ?x\<^sub>n = f ?y\<^sub>1 \ ?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 \ ?Q\<^sub>1 \ (?Q\<^sub>1 \ ?P\<^sub>2 \ ?Q\<^sub>2) \ + (?P\<^sub>1 \ ?P\<^sub>2) \ (?Q\<^sub>1 \ ?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 \ 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) \ (\x. x \ ?B \ ?P x \ ?Q x) \ + (\x \ ?A. ?P x) \ (\x \ ?B. ?Q x)"} + + \medskip This congruence rule for conditional expressions can + supply contextual information for simplifying the arms: + @{text [display] "?p = ?q \ (?q \ ?a = ?c) \ (\ ?q \ ?b = ?d) \ + (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 \ (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 diff -r a49f9428aba4 -r 003a01272d28 doc-src/IsarRef/Thy/document/Generic.tex --- 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% diff -r a49f9428aba4 -r 003a01272d28 doc-src/IsarRef/style.sty --- 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}} diff -r a49f9428aba4 -r 003a01272d28 doc-src/Ref/simplifier.tex --- 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 : diff -r a49f9428aba4 -r 003a01272d28 lib/texinputs/isabelle.sty --- 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}{%