Slides/document/root.tex
branchNominal2-Isabelle2011-1
changeset 3070 4b4742aa43f2
parent 3069 78d828f43cdf
child 3071 11f6a561eb4b
--- 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<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=`\`%
-
-\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: 
-