--- a/Nominal/ExLet.thy Thu Apr 01 01:05:05 2010 +0200
+++ b/Nominal/ExLet.thy Thu Apr 01 03:28:28 2010 +0200
@@ -6,7 +6,7 @@
atom_decl name
-ML {* val _ = recursive := false *}
+ML {* val _ = recursive := true *}
ML {* val _ = alpha_type := AlphaLst *}
nominal_datatype trm =
Vr "name"
@@ -36,6 +36,7 @@
(*thm trm_lts.supp*)
thm trm_lts.fv[simplified trm_lts.supp(1-2)]
+
primrec
permute_bn_raw
where
--- a/Paper/Paper.thy Thu Apr 01 01:05:05 2010 +0200
+++ b/Paper/Paper.thy Thu Apr 01 03:28:28 2010 +0200
@@ -18,9 +18,9 @@
supp ("supp _" [78] 73) and
uminus ("-_" [78] 73) and
If ("if _ then _ else _" 10) and
- alpha_gen ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{set}}$}}>\<^bsup>_,_,_\<^esup> _") and
- alpha_lst ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_,_,_\<^esup> _") and
- alpha_res ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{res}}$}}>\<^bsup>_,_,_\<^esup> _") and
+ alpha_gen ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and
+ alpha_lst ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_, _, _\<^esup> _") and
+ alpha_res ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{res}}$}}>\<^bsup>_, _, _\<^esup> _") and
abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
fv ("fv'(_')" [100] 100) and
equal ("=") and
@@ -31,13 +31,14 @@
Cons ("_::_" [78,77] 73) and
supp_gen ("aux _" [1000] 10) and
alpha_bn ("_ \<approx>bn _")
-
(*>*)
section {* Introduction *}
text {*
+ @{text "(1, (2, 3))"}
+
So far, Nominal Isabelle provides a mechanism for constructing
alpha-equated terms, for example
@@ -733,14 +734,11 @@
and $\approx_{\textit{abs\_res}}$). We can show that these relations are equivalence
relations and equivariant.
- \begin{lemma}\label{alphaeq} The relations
- $\approx_{\textit{abs\_set}}$,
- $\approx_{\textit{abs\_list}}$
- and $\approx_{\textit{abs\_res}}$
- are equivalence
- relations, and if @{term "abs_set (as, x) (bs, y)"} then also
- @{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> y)"} (similarly for
- the other two relations).
+ \begin{lemma}\label{alphaeq}
+ The relations $\approx_{\textit{abs\_set}}$, $\approx_{\textit{abs\_list}}$
+ and $\approx_{\textit{abs\_res}}$ are equivalence relations, and if @{term
+ "abs_set (as, x) (bs, y)"} then also @{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet>
+ bs, p \<bullet> y)"} (similarly for the other two relations).
\end{lemma}
\begin{proof}
@@ -1343,7 +1341,16 @@
*}
(*<*)
consts alpha_ty ::'a
-notation alpha_ty ("\<approx>ty")
+consts alpha_trm ::'a
+consts fv_trm :: 'a
+consts alpha_trm2 ::'a
+consts fv_trm2 :: 'a
+notation (latex output)
+ alpha_ty ("\<approx>ty") and
+ alpha_trm ("\<approx>\<^bsub>trm\<^esub>") and
+ fv_trm ("fv\<^bsub>trm\<^esub>") and
+ alpha_trm2 ("\<approx>\<^bsub>assn\<^esub> \<otimes> \<approx>\<^bsub>trm\<^esub>") and
+ fv_trm2 ("fv\<^bsub>assn\<^esub> \<oplus> fv\<^bsub>trm\<^esub>")
(*>*)
text {*
\begin{itemize}
@@ -1399,7 +1406,7 @@
recursive arguments of the term-constructor. If they are non-recursive arguments
then we generate just @{text "x\<^isub>i = y\<^isub>i"}.
- TODO
+ {\bf TODO (I do not understand the definition below yet).}
The alpha-equivalence relations for binding functions are similar to the alpha-equivalences
for their respective types, the difference is that they ommit checking the arguments that
@@ -1418,23 +1425,81 @@
\end{tabular}
\end{center}
+ Again lets take a look at an example for these definitions. For \eqref{letrecs}
+ we have three relations, namely $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
+ $\approx_{\textit{bn}}$, with the clauses as follows:
+
+ \begin{center}
+ \begin{tabular}{@ {}c @ {}}
+ \infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}
+ {@{text "as \<approx>\<^bsub>bn\<^esub> as'"} & @{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fv_trm p (bn as', t')"}}\smallskip\\
+ \infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}}
+ {@{term "\<exists>p. (bn as, (as, t)) \<approx>lst alpha_trm2 fv_trm2 p (bn as', (as', t'))"}}
+ \end{tabular}
+ \end{center}
+
+ \begin{center}
+ \begin{tabular}{@ {}c @ {}}
+ \infer{@{text "ANil \<approx>\<^bsub>assn\<^esub> ANil"}}{}\\
+ \infer{@{text "ACons a t as \<approx>\<^bsub>assn\<^esub> ACons a' t' as"}}
+ {@{text "a = a'"} & @{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>assn\<^esub> as'"}}\medskip\\
+ \end{tabular}
+ \end{center}
+
+ \begin{center}
+ \begin{tabular}{@ {}c @ {}}
+ \infer{@{text "ANil \<approx>\<^bsub>bn\<^esub> ANil"}}{}\\
+ \infer{@{text "ACons a t as \<approx>\<^bsub>bn\<^esub> ACons a' t' as"}}
+ {@{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\medskip\\
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ Note the difference between $\approx_{\textit{assn}}$ and
+ $\approx_{\textit{bn}}$: the latter only ``tracks'' alpha-equivalence of
+ the components in an assignment that are \emph{not} bound. Therefore we have
+ a $\approx_{\textit{bn}}$-premise in the clause for @{text "Let"} (which is
+ a non-recursive binder), since the terms inside an assignment are not meant
+ to be under the binder. Such a premise is not needed in @{text "Let_rec"},
+ because there everything from the assignment is under the binder.
*}
-section {* The Lifting of Definitions and Properties *}
+section {* Establishing the Reasoning Infrastructure *}
text {*
- To define the quotient types we first need to show that the defined
- relations are equivalence relations.
+ Having made all these definition for raw terms, we can start to introduce
+ the resoning infrastructure for the specified types. For this we first
+ have to show that the alpha-equivalence relation defined in the previous
+ sections are indeed equivalence relations.
- \begin{lemma} The relations @{text "\<approx>\<^isub>1 \<dots> \<approx>\<^isub>1"} and @{text "\<approx>bn\<^isub>1 \<dots> \<approx>bn\<^isub>m"}
- defined as above are equivalence relations and are equivariant.
+ \begin{lemma}
+ Given the raw types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"} and binding functions
+ @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, the relations @{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"} and
+ @{text "\<approx>bn\<^isub>1 \<dots> \<approx>bn\<^isub>m"} are equivalence relations and equivariant.
\end{lemma}
- \begin{proof} Reflexivity by induction on the raw datatype. Symmetry,
- transitivity and equivariance by induction on the alpha equivalence
- relation. Using lemma \ref{alphaeq}, the conditions follow by simple
- calculations. \end{proof}
+
+ \begin{proof}
+ The proof is by induction over the definitions. The non-trivial
+ cases involves premises build up by $\approx_{\textit{set}}$,
+ $\approx_{\textit{res}}$ and $\approx_{\textit{list}}$. They
+ can be dealt with like in Lemma~\ref{alphaeq}.
+ \end{proof}
- \noindent We then define the quotient types @{text "ty\<^isub>1\<^isup>\<alpha> \<dots> ty\<^isub>n\<^isup>\<alpha>"}. To lift
+ \noindent
+ We can feed this lemma into our quotient package and obtain new types @{text
+ "ty"}$^\alpha_{1..n}$ representing alpha-equated terms of types @{text
+ "ty"}$_{1..n}$. We also obtain definitions for the term-constructors @{text
+ "C"}$^\alpha_{1..m}$ from the raw term-constructors @{text
+ "C"}$_{1..m}$. Similarly for the free-variable functions @{text
+ "fv_ty"}$^\alpha_{1..n}$ and the binding functions @{text
+ "bn"}$^\alpha_{1..k}$. However, these definitions are of not much use for the
+ user, since the are formulated in terms of the isomorphism we obtained by
+ cerating a new type in Isabelle/HOL (remember the picture shown in the
+ Introduction).
+
+ {\bf TODO below.}
+
+ then define the quotient types @{text "ty\<^isub>1\<^isup>\<alpha> \<dots> ty\<^isub>n\<^isup>\<alpha>"}. To lift
the raw definitions to the quotient type, we need to prove that they
\emph{respect} the relation. We follow the definition of respectfullness given
by Homeier~\cite{Homeier05}. The intuition behind a respectfullness condition
@@ -1572,28 +1637,8 @@
permutations on the lifted type and the lifted defining eqautions of @{text "\<bullet>bn"}.
\end{proof}
-
-
*}
-(* @{thm "ACons_subst[no_vars]"}*)
-
-text {*
-%%% FIXME: The restricions should have already been described in previous sections?
- Restrictions
-
- \begin{itemize}
- \item non-emptiness
- \item positive datatype definitions
- \item finitely supported abstractions
- \item respectfulness of the bn-functions\bigskip
- \item binders can only have a ``single scope''
- \item all bindings must have the same mode
- \end{itemize}
-*}
-
-section {* Examples *}
-
text {*
\begin{figure}
@@ -1629,7 +1674,7 @@
$|$~@{text "LAM_cty cv::cvar ckind t::trm"} \isacommand{bind}~@{text "cv"}~\isacommand{in}~@{text t}\\
$|$~@{text "App_ty trm ty"}~$|$~@{text "App_cty trm cty"}~$|$~@{text "App trm trm"}\\
$|$~@{text "Lam v::var ty t::trm"} \isacommand{bind}~@{text "v"}~\isacommand{in}~@{text t}\\
- $|$~@{text "Let x::var ty trm t::trm"} \isacommand{bind}~{text x}~\isacommand{in}~{text t}\\
+ $|$~@{text "Let x::var ty trm t::trm"} \isacommand{bind}~@{text x}~\isacommand{in}~@{text t}\\
$|$~@{text "Case trm assoc_lst"}~$|$~@{text "Cast trm co"}\\
\isacommand{and}~@{text "assoc_lst ="}\\
\phantom{$|$}~@{text ANil}~%
@@ -1657,14 +1702,20 @@
$|$~@{text "bv3 (TVCKCons c cty tl) = (atom c)::(bv3 tl)"}\\
\end{tabular}
\end{boxedminipage}
- \caption{\label{nominalcorehas}}
+ \caption{The nominal datatype declaration for Core-Haskell. At the moment we
+ do not support nested types; therefore we explicitly have to unfold the
+ lists @{text "co_lst"}, @{text "assoc_lst"} and so on. This will be improved
+ in a future version of Nominal Isabelle. Apart from that, the
+ declaration follows closely the original in Figure~\ref{corehas}. The
+ point of our work is that having made such a declaration one obtains
+ automatically a reasoning infrastructure for Core-Haskell.\label{nominalcorehas}}
\end{figure}
*}
-
+(* @{thm "ACons_subst[no_vars]"}*)
-section {* Adequacy *}
+section {* Strong Induction Principles *}
section {* Related Work *}
@@ -1698,8 +1749,22 @@
The reasoning there turned out to be quite complex.
Ott is better with list dot specifications; subgrammars, is untyped;
+*}
+
+text {*
+%%% FIXME: The restricions should have already been described in previous sections?
+ Restrictions
+
+ \begin{itemize}
+ \item non-emptiness
+ \item positive datatype definitions
+ \item finitely supported abstractions
+ \item respectfulness of the bn-functions\bigskip
+ \item binders can only have a ``single scope''
+ \item all bindings must have the same mode
+ \end{itemize}
+*}
-*}
section {* Conclusion *}
@@ -1718,9 +1783,7 @@
the Mercurial repository linked at
\href{http://isabelle.in.tum.de/nominal/download}
{http://isabelle.in.tum.de/nominal/download}.\medskip
-*}
-text {*
\noindent
{\bf Acknowledgements:} We are very grateful to Andrew Pitts for
many discussions about Nominal Isabelle. We thank Peter Sewell for
@@ -1728,11 +1791,7 @@
also for patiently explaining some of the finer points about the abstract
definitions and about the implementation of the Ott-tool. We
also thank Stephanie Weirich for suggesting to separate the subgrammars
- of kinds and types in our Core-Haskell example.
-
-
-
-
+ of kinds and types in our Core-Haskell example.
*}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/document/proof.sty Thu Apr 01 03:28:28 2010 +0200
@@ -0,0 +1,278 @@
+% proof.sty (Proof Figure Macros)
+%
+% version 3.0 (for both LaTeX 2.09 and LaTeX 2e)
+% Mar 6, 1997
+% Copyright (C) 1990 -- 1997, Makoto Tatsuta (tatsuta@kusm.kyoto-u.ac.jp)
+%
+% This program is free software; you can redistribute it or modify
+% it under the terms of the GNU General Public License as published by
+% the Free Software Foundation; either versions 1, or (at your option)
+% any later version.
+%
+% This program is distributed in the hope that it will be useful
+% but WITHOUT ANY WARRANTY; without even the implied warranty of
+% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+% GNU General Public License for more details.
+%
+% Usage:
+% In \documentstyle, specify an optional style `proof', say,
+% \documentstyle[proof]{article}.
+%
+% The following macros are available:
+%
+% In all the following macros, all the arguments such as
+% <Lowers> and <Uppers> are processed in math mode.
+%
+% \infer<Lower><Uppers>
+% draws an inference.
+%
+% Use & in <Uppers> to delimit upper formulae.
+% <Uppers> consists more than 0 formulae.
+%
+% \infer returns \hbox{ ... } or \vbox{ ... } and
+% sets \@LeftOffset and \@RightOffset globally.
+%
+% \infer[<Label>]<Lower><Uppers>
+% draws an inference labeled with <Label>.
+%
+% \infer*<Lower><Uppers>
+% draws a many step deduction.
+%
+% \infer*[<Label>]<Lower><Uppers>
+% draws a many step deduction labeled with <Label>.
+%
+% \infer=<Lower><Uppers>
+% draws a double-ruled deduction.
+%
+% \infer=[<Label>]<Lower><Uppers>
+% draws a double-ruled deduction labeled with <Label>.
+%
+% \deduce<Lower><Uppers>
+% draws an inference without a rule.
+%
+% \deduce[<Proof>]<Lower><Uppers>
+% draws a many step deduction with a proof name.
+%
+% Example:
+% If you want to write
+% B C
+% -----
+% A D
+% ----------
+% E
+% use
+% \infer{E}{
+% A
+% &
+% \infer{D}{B & C}
+% }
+%
+
+% Style Parameters
+
+\newdimen\inferLineSkip \inferLineSkip=2pt
+\newdimen\inferLabelSkip \inferLabelSkip=5pt
+\def\inferTabSkip{\quad}
+
+% Variables
+
+\newdimen\@LeftOffset % global
+\newdimen\@RightOffset % global
+\newdimen\@SavedLeftOffset % safe from users
+
+\newdimen\UpperWidth
+\newdimen\LowerWidth
+\newdimen\LowerHeight
+\newdimen\UpperLeftOffset
+\newdimen\UpperRightOffset
+\newdimen\UpperCenter
+\newdimen\LowerCenter
+\newdimen\UpperAdjust
+\newdimen\RuleAdjust
+\newdimen\LowerAdjust
+\newdimen\RuleWidth
+\newdimen\HLabelAdjust
+\newdimen\VLabelAdjust
+\newdimen\WidthAdjust
+
+\newbox\@UpperPart
+\newbox\@LowerPart
+\newbox\@LabelPart
+\newbox\ResultBox
+
+% Flags
+
+\newif\if@inferRule % whether \@infer draws a rule.
+\newif\if@DoubleRule % whether \@infer draws doulbe rules.
+\newif\if@ReturnLeftOffset % whether \@infer returns \@LeftOffset.
+\newif\if@MathSaved % whether inner math mode where \infer or
+ % \deduce appears.
+
+% Special Fonts
+
+\def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@
+ \vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}}
+
+% Math Save Macros
+%
+% \@SaveMath is called in the very begining of toplevel macros
+% which are \infer and \deduce.
+% \@RestoreMath is called in the very last before toplevel macros end.
+% Remark \infer and \deduce ends calling \@infer.
+
+\def\@SaveMath{\@MathSavedfalse \ifmmode \ifinner
+ \relax $\relax \@MathSavedtrue \fi\fi }
+
+\def\@RestoreMath{\if@MathSaved \relax $\relax\fi }
+
+% Macros
+
+% Renaming @ifnextchar and @ifnch of LaTeX2e to @IFnextchar and @IFnch.
+
+\def\@IFnextchar#1#2#3{%
+ \let\reserved@e=#1\def\reserved@a{#2}\def\reserved@b{#3}\futurelet
+ \reserved@c\@IFnch}
+\def\@IFnch{\ifx \reserved@c \@sptoken \let\reserved@d\@xifnch
+ \else \ifx \reserved@c \reserved@e\let\reserved@d\reserved@a\else
+ \let\reserved@d\reserved@b\fi
+ \fi \reserved@d}
+
+\def\@ifEmpty#1#2#3{\def\@tempa{\@empty}\def\@tempb{#1}\relax
+ \ifx \@tempa \@tempb #2\else #3\fi }
+
+\def\infer{\@SaveMath \@IFnextchar *{\@inferSteps}{\relax
+ \@IFnextchar ={\@inferDoubleRule}{\@inferOneStep}}}
+
+\def\@inferOneStep{\@inferRuletrue \@DoubleRulefalse
+ \@IFnextchar [{\@infer}{\@infer[\@empty]}}
+
+\def\@inferDoubleRule={\@inferRuletrue \@DoubleRuletrue
+ \@IFnextchar [{\@infer}{\@infer[\@empty]}}
+
+\def\@inferSteps*{\@IFnextchar [{\@@inferSteps}{\@@inferSteps[\@empty]}}
+
+\def\@@inferSteps[#1]{\@deduce{#1}[\DeduceSym]}
+
+\def\deduce{\@SaveMath \@IFnextchar [{\@deduce{\@empty}}
+ {\@inferRulefalse \@infer[\@empty]}}
+
+% \@deduce<Proof Label>[<Proof>]<Lower><Uppers>
+
+\def\@deduce#1[#2]#3#4{\@inferRulefalse
+ \@infer[\@empty]{#3}{\@SaveMath \@infer[{#1}]{#2}{#4}}}
+
+% \@infer[<Label>]<Lower><Uppers>
+% If \@inferRuletrue, it draws a rule and <Label> is right to
+% a rule. In this case, if \@DoubleRuletrue, it draws
+% double rules.
+%
+% Otherwise, draws no rule and <Label> is right to <Lower>.
+
+\def\@infer[#1]#2#3{\relax
+% Get parameters
+ \if@ReturnLeftOffset \else \@SavedLeftOffset=\@LeftOffset \fi
+ \setbox\@LabelPart=\hbox{$#1$}\relax
+ \setbox\@LowerPart=\hbox{$#2$}\relax
+%
+ \global\@LeftOffset=0pt
+ \setbox\@UpperPart=\vbox{\tabskip=0pt \halign{\relax
+ \global\@RightOffset=0pt \@ReturnLeftOffsettrue $##$&&
+ \inferTabSkip
+ \global\@RightOffset=0pt \@ReturnLeftOffsetfalse $##$\cr
+ #3\cr}}\relax
+% Here is a little trick.
+% \@ReturnLeftOffsettrue(false) influences on \infer or
+% \deduce placed in ## locally
+% because of \@SaveMath and \@RestoreMath.
+ \UpperLeftOffset=\@LeftOffset
+ \UpperRightOffset=\@RightOffset
+% Calculate Adjustments
+ \LowerWidth=\wd\@LowerPart
+ \LowerHeight=\ht\@LowerPart
+ \LowerCenter=0.5\LowerWidth
+%
+ \UpperWidth=\wd\@UpperPart \advance\UpperWidth by -\UpperLeftOffset
+ \advance\UpperWidth by -\UpperRightOffset
+ \UpperCenter=\UpperLeftOffset
+ \advance\UpperCenter by 0.5\UpperWidth
+%
+ \ifdim \UpperWidth > \LowerWidth
+ % \UpperCenter > \LowerCenter
+ \UpperAdjust=0pt
+ \RuleAdjust=\UpperLeftOffset
+ \LowerAdjust=\UpperCenter \advance\LowerAdjust by -\LowerCenter
+ \RuleWidth=\UpperWidth
+ \global\@LeftOffset=\LowerAdjust
+%
+ \else % \UpperWidth <= \LowerWidth
+ \ifdim \UpperCenter > \LowerCenter
+%
+ \UpperAdjust=0pt
+ \RuleAdjust=\UpperCenter \advance\RuleAdjust by -\LowerCenter
+ \LowerAdjust=\RuleAdjust
+ \RuleWidth=\LowerWidth
+ \global\@LeftOffset=\LowerAdjust
+%
+ \else % \UpperWidth <= \LowerWidth
+ % \UpperCenter <= \LowerCenter
+%
+ \UpperAdjust=\LowerCenter \advance\UpperAdjust by -\UpperCenter
+ \RuleAdjust=0pt
+ \LowerAdjust=0pt
+ \RuleWidth=\LowerWidth
+ \global\@LeftOffset=0pt
+%
+ \fi\fi
+% Make a box
+ \if@inferRule
+%
+ \setbox\ResultBox=\vbox{
+ \moveright \UpperAdjust \box\@UpperPart
+ \nointerlineskip \kern\inferLineSkip
+ \if@DoubleRule
+ \moveright \RuleAdjust \vbox{\hrule width\RuleWidth
+ \kern 1pt\hrule width\RuleWidth}\relax
+ \else
+ \moveright \RuleAdjust \vbox{\hrule width\RuleWidth}\relax
+ \fi
+ \nointerlineskip \kern\inferLineSkip
+ \moveright \LowerAdjust \box\@LowerPart }\relax
+%
+ \@ifEmpty{#1}{}{\relax
+%
+ \HLabelAdjust=\wd\ResultBox \advance\HLabelAdjust by -\RuleAdjust
+ \advance\HLabelAdjust by -\RuleWidth
+ \WidthAdjust=\HLabelAdjust
+ \advance\WidthAdjust by -\inferLabelSkip
+ \advance\WidthAdjust by -\wd\@LabelPart
+ \ifdim \WidthAdjust < 0pt \WidthAdjust=0pt \fi
+%
+ \VLabelAdjust=\dp\@LabelPart
+ \advance\VLabelAdjust by -\ht\@LabelPart
+ \VLabelAdjust=0.5\VLabelAdjust \advance\VLabelAdjust by \LowerHeight
+ \advance\VLabelAdjust by \inferLineSkip
+%
+ \setbox\ResultBox=\hbox{\box\ResultBox
+ \kern -\HLabelAdjust \kern\inferLabelSkip
+ \raise\VLabelAdjust \box\@LabelPart \kern\WidthAdjust}\relax
+%
+ }\relax % end @ifEmpty
+%
+ \else % \@inferRulefalse
+%
+ \setbox\ResultBox=\vbox{
+ \moveright \UpperAdjust \box\@UpperPart
+ \nointerlineskip \kern\inferLineSkip
+ \moveright \LowerAdjust \hbox{\unhbox\@LowerPart
+ \@ifEmpty{#1}{}{\relax
+ \kern\inferLabelSkip \unhbox\@LabelPart}}}\relax
+ \fi
+%
+ \global\@RightOffset=\wd\ResultBox
+ \global\advance\@RightOffset by -\@LeftOffset
+ \global\advance\@RightOffset by -\LowerWidth
+ \if@ReturnLeftOffset \else \global\@LeftOffset=\@SavedLeftOffset \fi
+%
+ \box\ResultBox
+ \@RestoreMath
+}
--- a/Paper/document/root.bib Thu Apr 01 01:05:05 2010 +0200
+++ b/Paper/document/root.bib Thu Apr 01 03:28:28 2010 +0200
@@ -11,7 +11,7 @@
title = "{T}he {L}ocally {N}ameless {R}epresentation",
year = "2009",
note = "To appear in J.~of Automated Reasoning.
- {http://arthur.chargueraud.org/research/2009/ln/}",
+ http://arthur.chargueraud.org/research/2009/ln",
}
@article{NaraschewskiNipkow99,
--- a/Paper/document/root.tex Thu Apr 01 01:05:05 2010 +0200
+++ b/Paper/document/root.tex Thu Apr 01 03:28:28 2010 +0200
@@ -10,7 +10,7 @@
\usepackage{ot1patch}
\usepackage{times}
\usepackage{boxedminipage}
-
+\usepackage{proof}
\urlstyle{rm}
\isabellestyle{it}