\documentclass[dvipsnames, 14pt,t]{beamer}
\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}
\nocite{*}
\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: