prio/Slides/document/root.tex
changeset 373 0679a84b11ad
parent 372 2c56b20032a7
child 374 01d223421ba0
--- a/prio/Slides/document/root.tex	Mon Dec 03 08:16:58 2012 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,147 +0,0 @@
-\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: 
-