diff -r 78d828f43cdf -r 4b4742aa43f2 Slides/document/root.tex --- a/Slides/document/root.tex Sat Dec 17 16:58:11 2011 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,167 +0,0 @@ -\usepackage{beamerthemeplainculight} -\usepackage[T1]{fontenc} -\usepackage{proof} -\usepackage{german} -\usepackage[latin1]{inputenc} -\usepackage{isabelle} -\usepackage{isabellesym} -%%\usepackage{mathpartir} -\usepackage[absolute,overlay]{textpos} -\usepackage{proof} -\usepackage{ifthen} -%%\usepackage{animate} -\usepackage{tikz} -\usepackage{pgf} -\usepackage{calc} -\usepackage{ulem} -%%%\newcommand{\uline}[1]{} -\usetikzlibrary{arrows} -\usetikzlibrary{automata} -\usetikzlibrary{shapes} -\usetikzlibrary{shadows} -\usetikzlibrary{positioning} -%%%\usetikzlibrary{mindmap} - -\usepackage{graphicx} -\usepackage{xcolor} - -% general math stuff -\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions -\newcommand{\dnn}{\stackrel{\mbox{\Large def}}{=}} -\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 - - - -% 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} -\renewcommand{\isasymequiv}{$\dn$} - -% mathpatir -%%\mprset{sep=1em} - - -% beamer stuff -\renewcommand{\slidecaption}{Salvador, 26.~August 2008} - - -% colours for Isar Code (in article mode everything is black and white) -\mode{ -\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
{ -\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=`\`% - -\let\oldisachardoublequoteopen=\isachardoublequoteopen -\let\oldisachardoublequoteclose=\isachardoublequoteclose -\let\oldisacharbackquoteopen=\isacharbackquoteopen -\let\oldisacharbackquoteclose=\isacharbackquoteclose -\newenvironment{innerdouble}% - {\oldisachardoublequoteopen \color{isacol:green}}% - {\color{isacol:black} \oldisachardoublequoteclose} -\newenvironment{innersingle}% -{\oldisacharbackquoteopen\color{isacol:green}}% -{\color{isacol:black}\oldisacharbackquoteclose} - -\renewcommand{\isachardoublequoteopen}{\egroup\begin{innerdouble}\bgroup} -\renewcommand{\isachardoublequoteclose}{\egroup\end{innerdouble}\bgroup} -\renewcommand{\isacharbackquoteopen}{\egroup\begin{innersingle}\bgroup} -\renewcommand{\isacharbackquoteclose}{\egroup\end{innersingle}\bgroup} - -%% 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: -