--- a/prio/IsaMakefile Thu Jun 21 15:04:48 2012 +0000
+++ b/prio/IsaMakefile Thu Jun 28 11:25:26 2012 +0000
@@ -2,7 +2,7 @@
## targets
default: itp
-all: session itp
+all: session itp slides1
## global settings
@@ -16,9 +16,24 @@
## Slides
+session1: Slides/ROOT1.ML \
+ Slides/document/root* \
+ Slides/Slides1.thy
+ @$(USEDIR) -D generated -f ROOT1.ML HOL Slides
+
+slides1: session1
+ rm -f Slides/generated/*.aux # otherwise latex will fall over
+ cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
+ cp Slides/generated/root.beamer.pdf Slides/slides.pdf
+
+# main files
+
session: ./ROOT.ML ./*.thy
@$(USEDIR) -b -D generated -f ROOT.ML HOL Prio
+
+# itp paper
+
itp: Paper/*.thy Paper/*.ML
@$(USEDIR) -D generated -f ROOT.ML Prio Paper
rm -f Paper/generated/*.aux # otherwise latex will fall over
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/prio/Slides/ROOT1.ML Thu Jun 28 11:25:26 2012 +0000
@@ -0,0 +1,7 @@
+(*show_question_marks := false;*)
+
+no_document use_thy "../CpsG";
+no_document use_thy "../ExtGG";
+no_document use_thy "~~/src/HOL/Library/LaTeXsugar";
+quick_and_dirty := true;
+use_thy "Slides1"
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/prio/Slides/Slides1.thy Thu Jun 28 11:25:26 2012 +0000
@@ -0,0 +1,550 @@
+(*<*)
+theory Slides1
+imports "../CpsG" "../ExtGG" "~~/src/HOL/Library/LaTeXsugar"
+begin
+
+notation (latex output)
+ set ("_") and
+ Cons ("_::/_" [66,65] 65)
+
+ML {*
+ open Printer;
+ show_question_marks_default := false;
+ *}
+
+notation (latex output)
+ Cons ("_::_" [78,77] 73) and
+ vt ("valid'_state") and
+ runing ("running") and
+ birthtime ("last'_set") and
+ If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
+ Prc ("'(_, _')") and
+ holding ("holds") and
+ waiting ("waits") and
+ Th ("T") and
+ Cs ("C") and
+ readys ("ready") and
+ depend ("RAG") and
+ preced ("prec") and
+ cpreced ("cprec") and
+ dependents ("dependants") and
+ cp ("cprec") and
+ holdents ("resources") and
+ original_priority ("priority") and
+ DUMMY ("\<^raw:\mbox{$\_\!\_$}>")
+
+(*>*)
+
+
+
+text_raw {*
+ \renewcommand{\slidecaption}{London, 28 June 2012}
+ \newcommand{\bl}[1]{#1}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}
+ \frametitle{%
+ \begin{tabular}{@ {}c@ {}}
+ \\[8mm]
+ \Large A Provably Correct Implementation\\[-3mm]
+ \Large of the Priority Inheritance Protocol\\[0mm]
+ \end{tabular}}
+
+ \begin{center}
+ \small Christian Urban\\
+ \end{center}
+
+ \begin{center}
+ \small joint work with Xingyuan Zhang and Chunhan Wu\medskip \\
+ \small \mbox{from the PLA University of Science and Technology in Nanjing}
+ \end{center}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Isabelle Theorem Prover}
+ My background:
+
+ \begin{itemize}
+ \item mechanical reasoning about languages with binders (Nominal)\medskip
+ \item Barendregt's variable convention can lead to \alert{false}\medskip
+ \item found a bug in a proof by Bob Harper and Frank Pfenning (CMU) on
+ LF (ACM TOCL, 2005)
+ \end{itemize}
+
+ \begin{textblock}{6}(6.5,12.5)
+ \includegraphics[scale=0.28]{isabelle1.png}
+ \end{textblock}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Real-Time OSes}
+ \large
+
+ \begin{itemize}
+ \item Processes have priorities\\[5mm]
+ \item Resources can be locked and unlocked
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Problem}
+ \Large
+
+ \begin{center}
+ \begin{tabular}{l}
+ \alert{H}igh-priority process\\[4mm]
+ \onslide<2->{\alert{M}edium-priority process}\\[4mm]
+ \alert{L}ow-priority process\\[4mm]
+ \end{tabular}
+ \end{center}
+
+ \onslide<3->{
+ \begin{itemize}
+ \item \alert{Priority Inversion} @{text "\<equiv>"} \alert{H $<$ L}
+ \item<4> avoid indefinite priority inversion
+ \end{itemize}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Mars Pathfinder Mission 1997}
+ \Large
+
+ \begin{center}
+ \includegraphics[scale=0.26]{pathfinder.jpg}
+ \end{center}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Solution}
+ \Large
+
+ \alert{Priority Inheritance Protocol (PIP):}
+
+ \begin{center}
+ \begin{tabular}{l}
+ \alert{H}igh-priority process\\[4mm]
+ \textcolor{gray}{Medium-priority process}\\[4mm]
+ \alert{L}ow-priority process\\[21mm]
+ {\normalsize (temporarily raise its priority)}
+ \end{tabular}
+ \end{center}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{\mbox{}}
+
+ \begin{quote}
+ ``Priority inheritance is neither ef$\!$ficient nor reliable.
+ Implementations are either incomplete (and unreliable)
+ or surprisingly complex and intrusive.''
+ \end{quote}\medskip
+
+ \begin{quote}
+ ``I observed in the kernel code (to my disgust), the Linux
+ PIP implementation is a nightmare: extremely heavy weight,
+ involving maintenance of a full wait-for graph, and requiring
+ updates for a range of events, including priority changes and
+ interruptions of wait operations.''
+ \end{quote}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{A Correctness ``Proof'' in 1990}
+ \Large
+
+ \begin{itemize}
+ \item a paper$^\star$
+ in 1990 ``proved'' the correctness of an algorithm for PIP\\[5mm]
+ \end{itemize}
+
+ \normalsize
+ \begin{quote}
+ \ldots{}after the thread (whose priority has been raised) completes its
+ critical section and releases the lock, it ``returns to its original
+ priority level''.
+ \end{quote}\bigskip
+
+ \small
+ $^\star$ in IEEE Transactions on Computers
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{}
+ \Large
+
+ \begin{center}
+ \begin{tabular}{l}
+ \alert{H}igh-priority process 1\\[2mm]
+ \alert{H}igh-priority process 2\\[8mm]
+ \alert{L}ow-priority process
+ \end{tabular}
+ \end{center}
+
+ \onslide<2->{
+ \begin{itemize}
+ \item Solution: \\Return to highest \alert{remaining} priority
+ \end{itemize}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Events}
+ \Large
+
+ \begin{center}
+ \begin{tabular}{l}
+ Create \textcolor{gray}{thread priority}\\
+ Exit \textcolor{gray}{thread}\\
+ Set \textcolor{gray}{thread priority}\\
+ Lock \textcolor{gray}{thread cs}\\
+ Unlock \textcolor{gray}{thread cs}\\
+ \end{tabular}
+ \end{center}\pause\medskip
+
+ \large
+ A \alert{state} is a list of events (that happened so far).
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Precedences}
+ \large
+
+ \begin{center}
+ \begin{tabular}{l}
+ @{thm preced_def[where thread="th"]}
+ \end{tabular}
+ \end{center}
+
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{RAGs}
+
+\begin{center}
+ \newcommand{\fnt}{\fontsize{7}{8}\selectfont}
+ \begin{tikzpicture}[scale=1]
+ %%\draw[step=2mm] (-3,2) grid (1,-1);
+
+ \node (A) at (0,0) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>0"}};
+ \node (B) at (2,0) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>1"}};
+ \node (C) at (4,0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>1"}};
+ \node (D) at (4,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>2"}};
+ \node (E) at (6,-0.7) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>2"}};
+ \node (E1) at (6, 0.2) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>3"}};
+ \node (F) at (8,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>3"}};
+
+ \draw [<-,line width=0.6mm] (A) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding} (B);
+ \draw [->,line width=0.6mm] (C) to node [pos=0.4,sloped,above=-0.5mm] {\fnt{}waiting} (B);
+ \draw [->,line width=0.6mm] (D) to node [pos=0.4,sloped,below=-0.5mm] {\fnt{}waiting} (B);
+ \draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,below=-0.5mm] {\fnt{}holding} (E);
+ \draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding} (E1);
+ \draw [->,line width=0.6mm] (F) to node [pos=0.45,sloped,below=-0.5mm] {\fnt{}waiting} (E);
+ \end{tikzpicture}
+ \end{center}\bigskip
+
+ \begin{center}
+ \begin{minipage}{0.8\linewidth}
+ \raggedleft
+ @{thm cs_depend_def}
+ \end{minipage}
+ \end{center}\pause
+
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Good Next Events}
+ %%\large
+
+ \begin{center}
+ @{thm[mode=Rule] thread_create[where thread=th]}\bigskip
+
+ @{thm[mode=Rule] thread_exit[where thread=th]}\bigskip
+
+ @{thm[mode=Rule] thread_set[where thread=th]}
+ \end{center}
+
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Good Next Events}
+ %%\large
+
+ \begin{center}
+ @{thm[mode=Rule] thread_P[where thread=th]}\bigskip
+
+ @{thm[mode=Rule] thread_V[where thread=th]}\bigskip
+ \end{center}
+
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Theorem}
+
+ \textcolor{gray}{``No indefinite priority inversion''}\bigskip
+
+ Theorem:$^\star$ If th is the thread with the highest precedence in state s,
+ then in every future state @{text "s'"} in which th is still
+ alive\smallskip
+
+
+ \begin{itemize}
+ \item th is blocked by a thread @{text "th'"} that was alive in s
+ \item @{text "th'"} held a resource in s, and
+ \item @{text "th'"} is running with the precedence of th.\bigskip
+ \end{itemize}
+
+ \small
+ $^\star$ modulo some further assumptions\bigskip\pause
+
+ It does not matter which process gets a released lock.
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[t]
+ \frametitle{Implementation}
+
+ s $=$ current state; @{text "s'"} $=$ next state\bigskip\bigskip
+
+ \alert{Create th prio}, \alert{Exit th}
+
+ \begin{itemize}
+ \item @{text "RAG s' = RAG s"}
+ \item precedences of descendants stay all the same
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[t]
+ \frametitle{Implementation}
+
+ s $=$ current state; @{text "s'"} $=$ next state\bigskip\bigskip
+
+ \alert{Set th prio}
+
+ \begin{itemize}
+ \item @{text "RAG s' = RAG s"}
+ \item we have to recalculate the precedence of the direct descendants
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[t]
+ \frametitle{Implementation}
+
+ s $=$ current state; @{text "s'"} $=$ next state\bigskip
+
+ \alert{Unlock th cs} where there is a thread to take over
+
+ \begin{itemize}
+ \item @{text "RAG s' = RAG s - {(C cs, T th), (T th', C cs)} \<union> {(C cs, T th')}"}
+ \item we have to recalculate the precedence of the direct descendants
+ \end{itemize}\bigskip
+
+ \alert{Unlock th cs} where no thread takes over
+
+ \begin{itemize}
+ \item @{text "RAG s' = RAG s - {(C cs, T th)}"}
+ \item no recalculation of precedences
+ \end{itemize}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[t]
+ \frametitle{Implementation}
+
+ s $=$ current state; @{text "s'"} $=$ next state\bigskip\bigskip
+
+ \alert{Lock th cs} where cs is not locked
+
+ \begin{itemize}
+ \item @{text "RAG s' = RAG s \<union> {(C cs, T th')}"}
+ \item no recalculation of precedences
+ \end{itemize}\bigskip
+
+ \alert{Lock th cs} where cs is locked
+
+ \begin{itemize}
+ \item @{text "RAG s' = RAG s - {(T th, C cs)}"}
+ \item we have to recalculate the precedence of the descendants
+ \end{itemize}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{PINTOS}
+
+ \begin{itemize}
+ \item \ldots{}small operating system developed at Stanford for teaching;
+ written in C\bigskip
+ \end{itemize}
+
+ \begin{center}
+ \begin{tabular}{|l@ {\hspace{2mm}}|l@ {\hspace{2mm}}|}
+ \hline
+ {\bf Event} & {\bf PINTOS function} \\
+ \hline
+ @{text Create} & @{text "thread_create"}\\
+ @{text Exit} & @{text "thread_exit"}\\
+ @{text Set} & @{text "thread_set_priority"}\\
+ @{text Lock} & @{text "lock_acquire"}\\
+ @{text Unlock} & @{text "lock_release"}\\
+ \hline
+ \end{tabular}
+ \end{center}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Conclusion}
+
+ \begin{itemize}
+ \item surprised how pleasant the experience was\medskip
+
+ \item no real specification existed for PIP\medskip
+
+ \item general technique (a ``hammer''):\\[2mm]
+ events, separation of good and bad configurations\medskip
+
+ \item scheduler in RT-Linux\medskip
+
+ \item multiprocessor case\medskip
+
+ \item other ``nails'' ? (networks, \ldots)
+ \end{itemize}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+(*<*)
+end
+(*>*)
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/prio/Slides/document/beamerthemeplaincu.sty Thu Jun 28 11:25:26 2012 +0000
@@ -0,0 +1,126 @@
+\ProvidesPackage{beamerthemeplaincu}[2003/11/07 ver 0.93]
+\NeedsTeXFormat{LaTeX2e}[1995/12/01]
+
+% Copyright 2003 by Till Tantau <tantau@cs.tu-berlin.de>.
+%
+% This program can be redistributed and/or modified under the terms
+% of the LaTeX Project Public License Distributed from CTAN
+% archives in directory macros/latex/base/lppl.txt.
+
+\newcommand{\slidecaption}{}
+
+\mode<presentation>
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% comic fonts fonts
+\DeclareFontFamily{T1}{comic}{}%
+\DeclareFontShape{T1}{comic}{m}{n}{<->s*[.9]comic8t}{}%
+\DeclareFontShape{T1}{comic}{m}{it}{<->s*[.9]comic8t}{}%
+\DeclareFontShape{T1}{comic}{m}{sc}{<->s*[.9]comic8t}{}%
+\DeclareFontShape{T1}{comic}{b}{n}{<->s*[.9]comicbd8t}{}%
+\DeclareFontShape{T1}{comic}{b}{it}{<->s*[.9]comicbd8t}{}%
+\DeclareFontShape{T1}{comic}{m}{sl}{<->ssub * comic/m/it}{}%
+\DeclareFontShape{T1}{comic}{b}{sc}{<->sub * comic/m/sc}{}%
+\DeclareFontShape{T1}{comic}{b}{sl}{<->ssub * comic/b/it}{}%
+\DeclareFontShape{T1}{comic}{bx}{n}{<->ssub * comic/b/n}{}%
+\DeclareFontShape{T1}{comic}{bx}{it}{<->ssub * comic/b/it}{}%
+\DeclareFontShape{T1}{comic}{bx}{sc}{<->sub * comic/m/sc}{}%
+\DeclareFontShape{T1}{comic}{bx}{sl}{<->ssub * comic/b/it}{}%
+%
+\renewcommand{\rmdefault}{comic}%
+\renewcommand{\sfdefault}{comic}%
+\renewcommand{\mathfamilydefault}{cmr}% mathfont should be still the old one
+%
+\DeclareMathVersion{bold}% mathfont needs to be bold
+\DeclareSymbolFont{operators}{OT1}{cmr}{b}{n}%
+\SetSymbolFont{operators}{bold}{OT1}{cmr}{b}{n}%
+\DeclareSymbolFont{letters}{OML}{cmm}{b}{it}%
+\SetSymbolFont{letters}{bold}{OML}{cmm}{b}{it}%
+\DeclareSymbolFont{symbols}{OMS}{cmsy}{b}{n}%
+\SetSymbolFont{symbols}{bold}{OMS}{cmsy}{b}{n}%
+\DeclareSymbolFont{largesymbols}{OMX}{cmex}{b}{n}%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% % Title page
+%\usetitlepagetemplate{
+% \vbox{}
+% \vfill
+% \begin{centering}
+% \Large\structure{\textrm{\textit{{\inserttitle}}}}
+% \vskip1em\par
+% \normalsize\insertauthor\vskip1em\par
+% {\scriptsize\insertinstitute\par}\par\vskip1em
+% \insertdate\par\vskip1.5em
+% \inserttitlegraphic
+% \end{centering}
+% \vfill
+% }
+
+ % Part page
+%\usepartpagetemplate{
+% \begin{centering}
+% \Large\structure{\textrm{\textit{\partname~\@Roman\c@part}}}
+% \vskip1em\par
+% \textrm{\textit{\insertpart}}\par
+% \end{centering}
+% }
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Frametitles
+\setbeamerfont{frametitle}{size={\huge}}
+\setbeamerfont{frametitle}{family={\usefont{T1}{ptm}{b}{n}}}
+\setbeamercolor{frametitle}{fg=gray,bg=white}
+
+\setbeamertemplate{frametitle}{%
+\vskip 2mm % distance from the top margin
+\hskip -3mm % distance from left margin
+\vbox{%
+\begin{minipage}{1.05\textwidth}%
+\centering%
+\insertframetitle%
+\end{minipage}}%
+}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Foot
+%
+\setbeamertemplate{navigation symbols}{}
+\usefoottemplate{%
+\vbox{%
+ \tinyline{%
+ \tiny\hfill\textcolor{gray!50}{\slidecaption{} --
+ p.~\insertframenumber/\inserttotalframenumber}}}%
+}
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\beamertemplateballitem
+\setlength\leftmargini{2mm}
+\setlength\leftmarginii{0.6cm}
+\setlength\leftmarginiii{1.5cm}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% blocks
+%\definecolor{cream}{rgb}{1,1,.65}
+\definecolor{cream}{rgb}{1,1,.8}
+\setbeamerfont{block title}{size=\normalsize}
+\setbeamercolor{block title}{fg=black,bg=cream}
+\setbeamercolor{block body}{fg=black,bg=cream}
+
+\setbeamertemplate{blocks}[rounded][shadow=true]
+
+\setbeamercolor{boxcolor}{fg=black,bg=cream}
+
+\mode
+<all>
+
+
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/prio/Slides/document/mathpartir.sty Thu Jun 28 11:25:26 2012 +0000
@@ -0,0 +1,446 @@
+% Mathpartir --- Math Paragraph for Typesetting Inference Rules
+%
+% Copyright (C) 2001, 2002, 2003, 2004, 2005 Didier Rémy
+%
+% Author : Didier Remy
+% Version : 1.2.0
+% Bug Reports : to author
+% Web Site : http://pauillac.inria.fr/~remy/latex/
+%
+% Mathpartir is free software; you can redistribute it and/or modify
+% it under the terms of the GNU General Public License as published by
+% the Free Software Foundation; either version 2, or (at your option)
+% any later version.
+%
+% Mathpartir 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
+% (http://pauillac.inria.fr/~remy/license/GPL).
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% File mathpartir.sty (LaTeX macros)
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{mathpartir}
+ [2005/12/20 version 1.2.0 Math Paragraph for Typesetting Inference Rules]
+
+%%
+
+%% Identification
+%% Preliminary declarations
+
+\RequirePackage {keyval}
+
+%% Options
+%% More declarations
+
+%% PART I: Typesetting maths in paragraphe mode
+
+%% \newdimen \mpr@tmpdim
+%% Dimens are a precious ressource. Uses seems to be local.
+\let \mpr@tmpdim \@tempdima
+
+% To ensure hevea \hva compatibility, \hva should expands to nothing
+% in mathpar or in inferrule
+\let \mpr@hva \empty
+
+%% normal paragraph parametters, should rather be taken dynamically
+\def \mpr@savepar {%
+ \edef \MathparNormalpar
+ {\noexpand \lineskiplimit \the\lineskiplimit
+ \noexpand \lineskip \the\lineskip}%
+ }
+
+\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em}
+\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em}
+\def \mpr@lineskip {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}
+\let \MathparLineskip \mpr@lineskip
+\def \mpr@paroptions {\MathparLineskip}
+\let \mpr@prebindings \relax
+
+\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em
+
+\def \mpr@goodbreakand
+ {\hskip -\mpr@andskip \penalty -1000\hskip \mpr@andskip}
+\def \mpr@and {\hskip \mpr@andskip}
+\def \mpr@andcr {\penalty 50\mpr@and}
+\def \mpr@cr {\penalty -10000\mpr@and}
+\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10}
+
+\def \mpr@bindings {%
+ \let \and \mpr@andcr
+ \let \par \mpr@andcr
+ \let \\\mpr@cr
+ \let \eqno \mpr@eqno
+ \let \hva \mpr@hva
+ }
+\let \MathparBindings \mpr@bindings
+
+% \@ifundefined {ignorespacesafterend}
+% {\def \ignorespacesafterend {\aftergroup \ignorespaces}
+
+\newenvironment{mathpar}[1][]
+ {$$\mpr@savepar \parskip 0em \hsize \linewidth \centering
+ \vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else
+ \noindent $\displaystyle\fi
+ \MathparBindings}
+ {\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend}
+
+\newenvironment{mathparpagebreakable}[1][]
+ {\begingroup
+ \par
+ \mpr@savepar \parskip 0em \hsize \linewidth \centering
+ \mpr@prebindings \mpr@paroptions #1%
+ \vskip \abovedisplayskip \vskip -\lineskip%
+ \ifmmode \else $\displaystyle\fi
+ \MathparBindings
+ }
+ {\unskip
+ \ifmmode $\fi \par\endgroup
+ \vskip \belowdisplayskip
+ \noindent
+ \ignorespacesafterend}
+
+% \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum
+% \wd0 < \hsize $$\box0$$\else \bmathpar #1\emathpar \fi}
+
+%%% HOV BOXES
+
+\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip
+ \vbox \bgroup \tabskip 0em \let \\ \cr
+ \halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup
+ \egroup}
+
+\def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize
+ \box0\else \mathvbox {#1}\fi}
+
+
+%% Part II -- operations on lists
+
+\newtoks \mpr@lista
+\newtoks \mpr@listb
+
+\long \def\mpr@cons #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
+{#2}\edef #2{\the \mpr@lista \the \mpr@listb}}
+
+\long \def\mpr@snoc #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
+{#2}\edef #2{\the \mpr@listb\the\mpr@lista}}
+
+\long \def \mpr@concat#1=#2\mpr@to#3{\mpr@lista \expandafter {#2}\mpr@listb
+\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}}
+
+\def \mpr@head #1\mpr@to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2}
+\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}}
+
+\def \mpr@flatten #1\mpr@to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2}
+\long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}}
+
+\def \mpr@makelist #1\mpr@to #2{\def \mpr@all {#1}%
+ \mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the
+ \mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty
+ \def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop
+ \mpr@flatten \mpr@all \mpr@to \mpr@one
+ \expandafter \mpr@snoc \mpr@one \mpr@to #2\expandafter \mpr@stripof
+ \mpr@all \mpr@stripend
+ \ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi
+ \ifx 1\mpr@isempty
+ \repeat
+}
+
+\def \mpr@rev #1\mpr@to #2{\let \mpr@tmp \empty
+ \def \\##1{\mpr@cons ##1\mpr@to \mpr@tmp}#1\let #2\mpr@tmp}
+
+%% Part III -- Type inference rules
+
+\newif \if@premisse
+\newbox \mpr@hlist
+\newbox \mpr@vlist
+\newif \ifmpr@center \mpr@centertrue
+\def \mpr@htovlist {%
+ \setbox \mpr@hlist
+ \hbox {\strut
+ \ifmpr@center \hskip -0.5\wd\mpr@hlist\fi
+ \unhbox \mpr@hlist}%
+ \setbox \mpr@vlist
+ \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist
+ \else \unvbox \mpr@vlist \box \mpr@hlist
+ \fi}%
+}
+% OLD version
+% \def \mpr@htovlist {%
+% \setbox \mpr@hlist
+% \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}%
+% \setbox \mpr@vlist
+% \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist
+% \else \unvbox \mpr@vlist \box \mpr@hlist
+% \fi}%
+% }
+
+\def \mpr@item #1{$\displaystyle #1$}
+\def \mpr@sep{2em}
+\def \mpr@blank { }
+\def \mpr@hovbox #1#2{\hbox
+ \bgroup
+ \ifx #1T\@premissetrue
+ \else \ifx #1B\@premissefalse
+ \else
+ \PackageError{mathpartir}
+ {Premisse orientation should either be T or B}
+ {Fatal error in Package}%
+ \fi \fi
+ \def \@test {#2}\ifx \@test \mpr@blank\else
+ \setbox \mpr@hlist \hbox {}%
+ \setbox \mpr@vlist \vbox {}%
+ \if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi
+ \let \@hvlist \empty \let \@rev \empty
+ \mpr@tmpdim 0em
+ \expandafter \mpr@makelist #2\mpr@to \mpr@flat
+ \if@premisse \mpr@rev \mpr@flat \mpr@to \@rev \else \let \@rev \mpr@flat \fi
+ \def \\##1{%
+ \def \@test {##1}\ifx \@test \empty
+ \mpr@htovlist
+ \mpr@tmpdim 0em %%% last bug fix not extensively checked
+ \else
+ \setbox0 \hbox{\mpr@item {##1}}\relax
+ \advance \mpr@tmpdim by \wd0
+ %\mpr@tmpdim 1.02\mpr@tmpdim
+ \ifnum \mpr@tmpdim < \hsize
+ \ifnum \wd\mpr@hlist > 0
+ \if@premisse
+ \setbox \mpr@hlist
+ \hbox {\unhbox0 \hskip \mpr@sep \unhbox \mpr@hlist}%
+ \else
+ \setbox \mpr@hlist
+ \hbox {\unhbox \mpr@hlist \hskip \mpr@sep \unhbox0}%
+ \fi
+ \else
+ \setbox \mpr@hlist \hbox {\unhbox0}%
+ \fi
+ \else
+ \ifnum \wd \mpr@hlist > 0
+ \mpr@htovlist
+ \mpr@tmpdim \wd0
+ \fi
+ \setbox \mpr@hlist \hbox {\unhbox0}%
+ \fi
+ \advance \mpr@tmpdim by \mpr@sep
+ \fi
+ }%
+ \@rev
+ \mpr@htovlist
+ \ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist
+ \fi
+ \egroup
+}
+
+%%% INFERENCE RULES
+
+\@ifundefined{@@over}{%
+ \let\@@over\over % fallback if amsmath is not loaded
+ \let\@@overwithdelims\overwithdelims
+ \let\@@atop\atop \let\@@atopwithdelims\atopwithdelims
+ \let\@@above\above \let\@@abovewithdelims\abovewithdelims
+ }{}
+
+%% The default
+
+\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em
+ $\displaystyle {#1\mpr@over #2}$}}
+\def \mpr@@nofraction #1#2{\hbox {\advance \hsize by -0.5em
+ $\displaystyle {#1\@@atop #2}$}}
+
+\let \mpr@fraction \mpr@@fraction
+
+%% A generic solution to arrow
+
+\def \mpr@make@fraction #1#2#3#4#5{\hbox {%
+ \def \mpr@tail{#1}%
+ \def \mpr@body{#2}%
+ \def \mpr@head{#3}%
+ \setbox1=\hbox{$#4$}\setbox2=\hbox{$#5$}%
+ \setbox3=\hbox{$\mkern -3mu\mpr@body\mkern -3mu$}%
+ \setbox3=\hbox{$\mkern -3mu \mpr@body\mkern -3mu$}%
+ \dimen0=\dp1\advance\dimen0 by \ht3\relax\dp1\dimen0\relax
+ \dimen0=\ht2\advance\dimen0 by \dp3\relax\ht2\dimen0\relax
+ \setbox0=\hbox {$\box1 \@@atop \box2$}%
+ \dimen0=\wd0\box0
+ \box0 \hskip -\dimen0\relax
+ \hbox to \dimen0 {$%
+ \mathrel{\mpr@tail}\joinrel
+ \xleaders\hbox{\copy3}\hfil\joinrel\mathrel{\mpr@head}%
+ $}}}
+
+%% Old stuff should be removed in next version
+\def \mpr@@nothing #1#2
+ {$\lower 0.01pt \mpr@@nofraction {#1}{#2}$}
+\def \mpr@@reduce #1#2{\hbox
+ {$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}}
+\def \mpr@@rewrite #1#2#3{\hbox
+ {$\lower 0.01pt \mpr@@fraction {#2}{#3}\mkern -8mu#1$}}
+\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}}
+
+\def \mpr@empty {}
+\def \mpr@inferrule
+ {\bgroup
+ \ifnum \linewidth<\hsize \hsize \linewidth\fi
+ \mpr@rulelineskip
+ \let \and \qquad
+ \let \hva \mpr@hva
+ \let \@rulename \mpr@empty
+ \let \@rule@options \mpr@empty
+ \let \mpr@over \@@over
+ \mpr@inferrule@}
+\newcommand {\mpr@inferrule@}[3][]
+ {\everymath={\displaystyle}%
+ \def \@test {#2}\ifx \empty \@test
+ \setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}%
+ \else
+ \def \@test {#3}\ifx \empty \@test
+ \setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}%
+ \else
+ \setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}%
+ \fi \fi
+ \def \@test {#1}\ifx \@test\empty \box0
+ \else \vbox
+%%% Suggestion de Francois pour les etiquettes longues
+%%% {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi
+ {\hbox {\RefTirName {#1}}\box0}\fi
+ \egroup}
+
+\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}}
+
+% They are two forms
+% \inferrule [label]{[premisses}{conclusions}
+% or
+% \inferrule* [options]{[premisses}{conclusions}
+%
+% Premisses and conclusions are lists of elements separated by \\
+% Each \\ produces a break, attempting horizontal breaks if possible,
+% and vertical breaks if needed.
+%
+% An empty element obtained by \\\\ produces a vertical break in all cases.
+%
+% The former rule is aligned on the fraction bar.
+% The optional label appears on top of the rule
+% The second form to be used in a derivation tree is aligned on the last
+% line of its conclusion
+%
+% The second form can be parameterized, using the key=val interface. The
+% folloiwng keys are recognized:
+%
+% width set the width of the rule to val
+% narrower set the width of the rule to val\hsize
+% before execute val at the beginning/left
+% lab put a label [Val] on top of the rule
+% lskip add negative skip on the right
+% left put a left label [Val]
+% Left put a left label [Val], ignoring its width
+% right put a right label [Val]
+% Right put a right label [Val], ignoring its width
+% leftskip skip negative space on the left-hand side
+% rightskip skip negative space on the right-hand side
+% vdots lift the rule by val and fill vertical space with dots
+% after execute val at the end/right
+%
+% Note that most options must come in this order to avoid strange
+% typesetting (in particular leftskip must preceed left and Left and
+% rightskip must follow Right or right; vdots must come last
+% or be only followed by rightskip.
+%
+
+%% Keys that make sence in all kinds of rules
+\def \mprset #1{\setkeys{mprset}{#1}}
+\define@key {mprset}{andskip}[]{\mpr@andskip=#1}
+\define@key {mprset}{lineskip}[]{\lineskip=#1}
+\define@key {mprset}{flushleft}[]{\mpr@centerfalse}
+\define@key {mprset}{center}[]{\mpr@centertrue}
+\define@key {mprset}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
+\define@key {mprset}{atop}[]{\let \mpr@fraction \mpr@@nofraction}
+\define@key {mprset}{myfraction}[]{\let \mpr@fraction #1}
+\define@key {mprset}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
+\define@key {mprset}{sep}{\def\mpr@sep{#1}}
+
+\newbox \mpr@right
+\define@key {mpr}{flushleft}[]{\mpr@centerfalse}
+\define@key {mpr}{center}[]{\mpr@centertrue}
+\define@key {mpr}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
+\define@key {mpr}{myfraction}[]{\let \mpr@fraction #1}
+\define@key {mpr}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
+\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
+ \advance \hsize by -\wd0\box0}
+\define@key {mpr}{width}{\hsize #1}
+\define@key {mpr}{sep}{\def\mpr@sep{#1}}
+\define@key {mpr}{before}{#1}
+\define@key {mpr}{lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
+\define@key {mpr}{Lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
+\define@key {mpr}{narrower}{\hsize #1\hsize}
+\define@key {mpr}{leftskip}{\hskip -#1}
+\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce}
+\define@key {mpr}{rightskip}
+ {\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}}
+\define@key {mpr}{LEFT}{\setbox0 \hbox {$#1$}\relax
+ \advance \hsize by -\wd0\box0}
+\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
+ \advance \hsize by -\wd0\box0}
+\define@key {mpr}{Left}{\llap{$\TirName {#1}\;$}}
+\define@key {mpr}{right}
+ {\setbox0 \hbox {$\;\TirName {#1}$}\relax \advance \hsize by -\wd0
+ \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
+\define@key {mpr}{RIGHT}
+ {\setbox0 \hbox {$#1$}\relax \advance \hsize by -\wd0
+ \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
+\define@key {mpr}{Right}
+ {\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\TirName {#1}$}}}
+\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}}
+\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}}
+
+\newcommand \mpr@inferstar@ [3][]{\setbox0
+ \hbox {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax
+ \setbox \mpr@right \hbox{}%
+ $\setkeys{mpr}{#1}%
+ \ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else
+ \mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi
+ \box \mpr@right \mpr@vdots$}
+ \setbox1 \hbox {\strut}
+ \@tempdima \dp0 \advance \@tempdima by -\dp1
+ \raise \@tempdima \box0}
+
+\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}}
+\newcommand \mpr@err@skipargs[3][]{}
+\def \mpr@inferstar*{\ifmmode
+ \let \@do \mpr@inferstar@
+ \else
+ \let \@do \mpr@err@skipargs
+ \PackageError {mathpartir}
+ {\string\inferrule* can only be used in math mode}{}%
+ \fi \@do}
+
+
+%%% Exports
+
+% Envirnonment mathpar
+
+\let \inferrule \mpr@infer
+
+% make a short name \infer is not already defined
+\@ifundefined {infer}{\let \infer \mpr@infer}{}
+
+\def \TirNameStyle #1{\small \textsc{#1}}
+\def \tir@name #1{\hbox {\small \TirNameStyle{#1}}}
+\let \TirName \tir@name
+\let \DefTirName \TirName
+\let \RefTirName \TirName
+
+%%% Other Exports
+
+% \let \listcons \mpr@cons
+% \let \listsnoc \mpr@snoc
+% \let \listhead \mpr@head
+% \let \listmake \mpr@makelist
+
+
+
+
+\endinput
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/prio/Slides/document/root.beamer.tex Thu Jun 28 11:25:26 2012 +0000
@@ -0,0 +1,12 @@
+\documentclass[14pt,t]{beamer}
+%%%\usepackage{pstricks}
+
+\input{root.tex}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% TeX-command-default: "Slides"
+%%% TeX-view-style: (("." "kghostview --landscape --scale 0.45 --geometry 605x505 %f"))
+%%% End:
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/prio/Slides/document/root.notes.tex Thu Jun 28 11:25:26 2012 +0000
@@ -0,0 +1,18 @@
+\documentclass[11pt]{article}
+%%\usepackage{pstricks}
+\usepackage{dina4}
+\usepackage{beamerarticle}
+\usepackage{times}
+\usepackage{hyperref}
+\usepackage{pgf}
+\usepackage{amssymb}
+\setjobnamebeamerversion{root.beamer}
+\input{root.tex}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% TeX-command-default: "Slides"
+%%% TeX-view-style: (("." "kghostview --landscape --scale 0.45 --geometry 605x505 %f"))
+%%% End:
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/prio/Slides/document/root.tex Thu Jun 28 11:25:26 2012 +0000
@@ -0,0 +1,147 @@
+\usepackage{beamerthemeplaincu}
+%%\usepackage{ulem}
+\usepackage[T1]{fontenc}
+\usepackage{proof}
+\usepackage[latin1]{inputenc}
+\usepackage{isabelle}
+\usepackage{isabellesym}
+\usepackage{mathpartir}
+\usepackage[absolute, overlay]{textpos}
+\usepackage{proof}
+\usepackage{ifthen}
+\usepackage{animate}
+\usepackage{tikz}
+\usepackage{pgf}
+\usetikzlibrary{arrows}
+\usetikzlibrary{automata}
+\usetikzlibrary{shapes}
+\usetikzlibrary{shadows}
+\usetikzlibrary{calc}
+
+% Isabelle configuration
+%%\urlstyle{rm}
+\isabellestyle{rm}
+\renewcommand{\isastyle}{\rm}%
+\renewcommand{\isastyleminor}{\rm}%
+\renewcommand{\isastylescript}{\footnotesize\rm\slshape}%
+\renewcommand{\isatagproof}{}
+\renewcommand{\endisatagproof}{}
+\renewcommand{\isamarkupcmt}[1]{#1}
+
+% Isabelle characters
+\renewcommand{\isacharunderscore}{\_}
+\renewcommand{\isacharbar}{\isamath{\mid}}
+\renewcommand{\isasymiota}{}
+\renewcommand{\isacharbraceleft}{\{}
+\renewcommand{\isacharbraceright}{\}}
+\renewcommand{\isacharless}{$\langle$}
+\renewcommand{\isachargreater}{$\rangle$}
+\renewcommand{\isasymsharp}{\isamath{\#}}
+\renewcommand{\isasymdots}{\isamath{...}}
+\renewcommand{\isasymbullet}{\act}
+
+% mathpatir
+\mprset{sep=1em}
+
+% general math stuff
+\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions
+\newcommand{\dnn}{\stackrel{\mbox{\Large def}}{=}}
+\renewcommand{\isasymequiv}{$\dn$}
+\renewcommand{\emptyset}{\varnothing}% nice round empty set
+\renewcommand{\Gamma}{\varGamma}
+\DeclareRobustCommand{\flqq}{\mbox{\guillemotleft}}
+\DeclareRobustCommand{\frqq}{\mbox{\guillemotright}}
+\newcommand{\smath}[1]{\textcolor{blue}{\ensuremath{#1}}}
+\newcommand{\fresh}{\mathrel{\#}}
+\newcommand{\act}{{\raisebox{-0.5mm}{\Large$\boldsymbol{\cdot}$}}}% swapping action
+\newcommand{\swap}[2]{(#1\,#2)}% swapping operation
+
+% beamer stuff
+\renewcommand{\slidecaption}{Salvador, 26.~August 2008}
+
+
+% colours for Isar Code (in article mode everything is black and white)
+\mode<presentation>{
+\definecolor{isacol:brown}{rgb}{.823,.411,.117}
+\definecolor{isacol:lightblue}{rgb}{.274,.509,.705}
+\definecolor{isacol:green}{rgb}{0,.51,0.14}
+\definecolor{isacol:red}{rgb}{.803,0,0}
+\definecolor{isacol:blue}{rgb}{0,0,.803}
+\definecolor{isacol:darkred}{rgb}{.545,0,0}
+\definecolor{isacol:black}{rgb}{0,0,0}}
+\mode<article>{
+\definecolor{isacol:brown}{rgb}{0,0,0}
+\definecolor{isacol:lightblue}{rgb}{0,0,0}
+\definecolor{isacol:green}{rgb}{0,0,0}
+\definecolor{isacol:red}{rgb}{0,0,0}
+\definecolor{isacol:blue}{rgb}{0,0,0}
+\definecolor{isacol:darkred}{rgb}{0,0,0}
+\definecolor{isacol:black}{rgb}{0,0,0}
+}
+
+
+\newcommand{\strong}[1]{{\bfseries {#1}}}
+\newcommand{\bluecmd}[1]{{\color{isacol:lightblue}{\strong{#1}}}}
+\newcommand{\browncmd}[1]{{\color{isacol:brown}{\strong{#1}}}}
+\newcommand{\redcmd}[1]{{\color{isacol:red}{\strong{#1}}}}
+
+\renewcommand{\isakeyword}[1]{%
+\ifthenelse{\equal{#1}{show}}{\browncmd{#1}}{%
+\ifthenelse{\equal{#1}{case}}{\browncmd{#1}}{%
+\ifthenelse{\equal{#1}{assume}}{\browncmd{#1}}{%
+\ifthenelse{\equal{#1}{obtain}}{\browncmd{#1}}{%
+\ifthenelse{\equal{#1}{fix}}{\browncmd{#1}}{%
+\ifthenelse{\equal{#1}{oops}}{\redcmd{#1}}{%
+\ifthenelse{\equal{#1}{thm}}{\redcmd{#1}}{%
+{\bluecmd{#1}}}}}}}}}}%
+
+% inner syntax colour
+\chardef\isachardoublequoteopen=`\"%
+\chardef\isachardoublequoteclose=`\"%
+\chardef\isacharbackquoteopen=`\`%
+\chardef\isacharbackquoteclose=`\`%
+\newenvironment{innersingle}%
+{\isacharbackquoteopen\color{isacol:green}}%
+{\color{isacol:black}\isacharbackquoteclose}
+\newenvironment{innerdouble}%
+{\isachardoublequoteopen\color{isacol:green}}%
+{\color{isacol:black}\isachardoublequoteclose}
+
+%% misc
+\newcommand{\gb}[1]{\textcolor{isacol:green}{#1}}
+\newcommand{\rb}[1]{\textcolor{red}{#1}}
+
+%% animations
+\newcounter{growcnt}
+\newcommand{\grow}[2]
+{\begin{tikzpicture}[baseline=(n.base)]%
+ \node[scale=(0.1 *#1 + 0.001),inner sep=0pt] (n) {#2};
+ \end{tikzpicture}%
+}
+
+%% isatabbing
+%\renewcommand{\isamarkupcmt}[1]%
+%{\ifthenelse{\equal{TABSET}{#1}}{\=}%
+% {\ifthenelse{\equal{TAB}{#1}}{\>}%
+% {\ifthenelse{\equal{NEWLINE}{#1}}{\\}%
+% {\ifthenelse{\equal{DOTS}{#1}}{\ldots}{\isastylecmt--- {#1}}}%
+% }%
+% }%
+%}%
+
+
+\newenvironment{isatabbing}%
+{\renewcommand{\isanewline}{\\}\begin{tabbing}}%
+{\end{tabbing}}
+
+\begin{document}
+\input{session}
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% TeX-command-default: "Slides"
+%%% TeX-view-style: (("." "kghostview --landscape --scale 0.45 --geometry 605x505 %f"))
+%%% End:
+
Binary file prio/Slides/slides.pdf has changed
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/prio/document/beamerthemeplaincu.sty Thu Jun 28 11:25:26 2012 +0000
@@ -0,0 +1,126 @@
+\ProvidesPackage{beamerthemeplaincu}[2003/11/07 ver 0.93]
+\NeedsTeXFormat{LaTeX2e}[1995/12/01]
+
+% Copyright 2003 by Till Tantau <tantau@cs.tu-berlin.de>.
+%
+% This program can be redistributed and/or modified under the terms
+% of the LaTeX Project Public License Distributed from CTAN
+% archives in directory macros/latex/base/lppl.txt.
+
+\newcommand{\slidecaption}{}
+
+\mode<presentation>
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% comic fonts fonts
+\DeclareFontFamily{T1}{comic}{}%
+\DeclareFontShape{T1}{comic}{m}{n}{<->s*[.9]comic8t}{}%
+\DeclareFontShape{T1}{comic}{m}{it}{<->s*[.9]comic8t}{}%
+\DeclareFontShape{T1}{comic}{m}{sc}{<->s*[.9]comic8t}{}%
+\DeclareFontShape{T1}{comic}{b}{n}{<->s*[.9]comicbd8t}{}%
+\DeclareFontShape{T1}{comic}{b}{it}{<->s*[.9]comicbd8t}{}%
+\DeclareFontShape{T1}{comic}{m}{sl}{<->ssub * comic/m/it}{}%
+\DeclareFontShape{T1}{comic}{b}{sc}{<->sub * comic/m/sc}{}%
+\DeclareFontShape{T1}{comic}{b}{sl}{<->ssub * comic/b/it}{}%
+\DeclareFontShape{T1}{comic}{bx}{n}{<->ssub * comic/b/n}{}%
+\DeclareFontShape{T1}{comic}{bx}{it}{<->ssub * comic/b/it}{}%
+\DeclareFontShape{T1}{comic}{bx}{sc}{<->sub * comic/m/sc}{}%
+\DeclareFontShape{T1}{comic}{bx}{sl}{<->ssub * comic/b/it}{}%
+%
+\renewcommand{\rmdefault}{comic}%
+\renewcommand{\sfdefault}{comic}%
+\renewcommand{\mathfamilydefault}{cmr}% mathfont should be still the old one
+%
+\DeclareMathVersion{bold}% mathfont needs to be bold
+\DeclareSymbolFont{operators}{OT1}{cmr}{b}{n}%
+\SetSymbolFont{operators}{bold}{OT1}{cmr}{b}{n}%
+\DeclareSymbolFont{letters}{OML}{cmm}{b}{it}%
+\SetSymbolFont{letters}{bold}{OML}{cmm}{b}{it}%
+\DeclareSymbolFont{symbols}{OMS}{cmsy}{b}{n}%
+\SetSymbolFont{symbols}{bold}{OMS}{cmsy}{b}{n}%
+\DeclareSymbolFont{largesymbols}{OMX}{cmex}{b}{n}%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% % Title page
+%\usetitlepagetemplate{
+% \vbox{}
+% \vfill
+% \begin{centering}
+% \Large\structure{\textrm{\textit{{\inserttitle}}}}
+% \vskip1em\par
+% \normalsize\insertauthor\vskip1em\par
+% {\scriptsize\insertinstitute\par}\par\vskip1em
+% \insertdate\par\vskip1.5em
+% \inserttitlegraphic
+% \end{centering}
+% \vfill
+% }
+
+ % Part page
+%\usepartpagetemplate{
+% \begin{centering}
+% \Large\structure{\textrm{\textit{\partname~\@Roman\c@part}}}
+% \vskip1em\par
+% \textrm{\textit{\insertpart}}\par
+% \end{centering}
+% }
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Frametitles
+\setbeamerfont{frametitle}{size={\huge}}
+\setbeamerfont{frametitle}{family={\usefont{T1}{ptm}{b}{n}}}
+\setbeamercolor{frametitle}{fg=gray,bg=white}
+
+\setbeamertemplate{frametitle}{%
+\vskip 2mm % distance from the top margin
+\hskip -3mm % distance from left margin
+\vbox{%
+\begin{minipage}{1.05\textwidth}%
+\centering%
+\insertframetitle%
+\end{minipage}}%
+}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Foot
+%
+\setbeamertemplate{navigation symbols}{}
+\usefoottemplate{%
+\vbox{%
+ \tinyline{%
+ \tiny\hfill\textcolor{gray!50}{\slidecaption{} --
+ p.~\insertframenumber/\inserttotalframenumber}}}%
+}
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\beamertemplateballitem
+\setlength\leftmargini{2mm}
+\setlength\leftmarginii{0.6cm}
+\setlength\leftmarginiii{1.5cm}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% blocks
+%\definecolor{cream}{rgb}{1,1,.65}
+\definecolor{cream}{rgb}{1,1,.8}
+\setbeamerfont{block title}{size=\normalsize}
+\setbeamercolor{block title}{fg=black,bg=cream}
+\setbeamercolor{block body}{fg=black,bg=cream}
+
+\setbeamertemplate{blocks}[rounded][shadow=true]
+
+\setbeamercolor{boxcolor}{fg=black,bg=cream}
+
+\mode
+<all>
+
+
+
+
+
+
Binary file prio/paper.pdf has changed