pip: Slides/document/root.tex@ed938e2246b9 (annotated)

18 598409a21f4c added nasa talk Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	1	\documentclass[dvipsnames, 14pt,t]{beamer}
0 110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	2	\usepackage{beamerthemeplaincu}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	3	%%\usepackage{ulem}
20 b56616fd88dd added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 18 diff changeset	4	%\usepackage[T1]{fontenc}
0 110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	5	\usepackage{proof}
20 b56616fd88dd added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 18 diff changeset	6	%\usepackage[latin1]{inputenc}
0 110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	7	\usepackage{isabelle}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	8	\usepackage{isabellesym}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	9	\usepackage{mathpartir}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	10	\usepackage[absolute, overlay]{textpos}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	11	\usepackage{proof}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	12	\usepackage{ifthen}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	13	\usepackage{animate}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	14	\usepackage{tikz}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	15	\usepackage{pgf}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	16	\usetikzlibrary{arrows}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	17	\usetikzlibrary{automata}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	18	\usetikzlibrary{shapes}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	19	\usetikzlibrary{shadows}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	20	\usetikzlibrary{calc}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	21
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	22	% Isabelle configuration
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	23	%%\urlstyle{rm}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	24	\isabellestyle{rm}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	25	\renewcommand{\isastyle}{\rm}%
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	26	\renewcommand{\isastyleminor}{\rm}%
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	27	\renewcommand{\isastylescript}{\footnotesize\rm\slshape}%
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	28	\renewcommand{\isatagproof}{}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	29	\renewcommand{\endisatagproof}{}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	30	\renewcommand{\isamarkupcmt}[1]{#1}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	31
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	32	% Isabelle characters
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	33	\renewcommand{\isacharunderscore}{\_}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	34	\renewcommand{\isacharbar}{\isamath{\mid}}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	35	\renewcommand{\isasymiota}{}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	36	\renewcommand{\isacharbraceleft}{\{}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	37	\renewcommand{\isacharbraceright}{\}}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	38	\renewcommand{\isacharless}{$\langle$}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	39	\renewcommand{\isachargreater}{$\rangle$}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	40	\renewcommand{\isasymsharp}{\isamath{\#}}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	41	\renewcommand{\isasymdots}{\isamath{...}}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	42	\renewcommand{\isasymbullet}{\act}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	43
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	44	% mathpatir
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	45	\mprset{sep=1em}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	46
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	47	% general math stuff
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	48	\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	49	\newcommand{\dnn}{\stackrel{\mbox{\Large def}}{=}}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	50	\renewcommand{\isasymequiv}{$\dn$}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	51	\renewcommand{\emptyset}{\varnothing}% nice round empty set
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	52	\renewcommand{\Gamma}{\varGamma}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	53	\DeclareRobustCommand{\flqq}{\mbox{\guillemotleft}}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	54	\DeclareRobustCommand{\frqq}{\mbox{\guillemotright}}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	55	\newcommand{\smath}[1]{\textcolor{blue}{\ensuremath{#1}}}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	56	\newcommand{\fresh}{\mathrel{\#}}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	57	\newcommand{\act}{{\raisebox{-0.5mm}{\Large$\boldsymbol{\cdot}$}}}% swapping action
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	58	\newcommand{\swap}[2]{(#1\,#2)}% swapping operation
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	59
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	60	% beamer stuff
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	61	\renewcommand{\slidecaption}{Salvador, 26.~August 2008}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	62
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	63
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	64	% colours for Isar Code (in article mode everything is black and white)
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	65	\mode<presentation>{
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	66	\definecolor{isacol:brown}{rgb}{.823,.411,.117}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	67	\definecolor{isacol:lightblue}{rgb}{.274,.509,.705}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	68	\definecolor{isacol:green}{rgb}{0,.51,0.14}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	69	\definecolor{isacol:red}{rgb}{.803,0,0}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	70	\definecolor{isacol:blue}{rgb}{0,0,.803}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	71	\definecolor{isacol:darkred}{rgb}{.545,0,0}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	72	\definecolor{isacol:black}{rgb}{0,0,0}}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	73	\mode<article>{
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	74	\definecolor{isacol:brown}{rgb}{0,0,0}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	75	\definecolor{isacol:lightblue}{rgb}{0,0,0}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	76	\definecolor{isacol:green}{rgb}{0,0,0}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	77	\definecolor{isacol:red}{rgb}{0,0,0}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	78	\definecolor{isacol:blue}{rgb}{0,0,0}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	79	\definecolor{isacol:darkred}{rgb}{0,0,0}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	80	\definecolor{isacol:black}{rgb}{0,0,0}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	81	}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	82
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	83
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	84	\newcommand{\strong}[1]{{\bfseries {#1}}}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	85	\newcommand{\bluecmd}[1]{{\color{isacol:lightblue}{\strong{#1}}}}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	86	\newcommand{\browncmd}[1]{{\color{isacol:brown}{\strong{#1}}}}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	87	\newcommand{\redcmd}[1]{{\color{isacol:red}{\strong{#1}}}}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	88
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	89	\renewcommand{\isakeyword}[1]{%
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	90	\ifthenelse{\equal{#1}{show}}{\browncmd{#1}}{%
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	91	\ifthenelse{\equal{#1}{case}}{\browncmd{#1}}{%
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	92	\ifthenelse{\equal{#1}{assume}}{\browncmd{#1}}{%
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	93	\ifthenelse{\equal{#1}{obtain}}{\browncmd{#1}}{%
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	94	\ifthenelse{\equal{#1}{fix}}{\browncmd{#1}}{%
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	95	\ifthenelse{\equal{#1}{oops}}{\redcmd{#1}}{%
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	96	\ifthenelse{\equal{#1}{thm}}{\redcmd{#1}}{%
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	97	{\bluecmd{#1}}}}}}}}}}%
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	98
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	99	% inner syntax colour
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	100	\chardef\isachardoublequoteopen=`\"%
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	101	\chardef\isachardoublequoteclose=`\"%
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	102	\chardef\isacharbackquoteopen=`\`%
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	103	\chardef\isacharbackquoteclose=`\`%
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	104	\newenvironment{innersingle}%
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	105	{\isacharbackquoteopen\color{isacol:green}}%
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	106	{\color{isacol:black}\isacharbackquoteclose}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	107	\newenvironment{innerdouble}%
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	108	{\isachardoublequoteopen\color{isacol:green}}%
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	109	{\color{isacol:black}\isachardoublequoteclose}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	110
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	111	%% misc
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	112	\newcommand{\gb}[1]{\textcolor{isacol:green}{#1}}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	113	\newcommand{\rb}[1]{\textcolor{red}{#1}}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	114
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	115	%% animations
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	116	\newcounter{growcnt}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	117	\newcommand{\grow}[2]
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	118	{\begin{tikzpicture}[baseline=(n.base)]%
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	119	\node[scale=(0.1 *#1 + 0.001),inner sep=0pt] (n) {#2};
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	120	\end{tikzpicture}%
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	121	}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	122
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	123	%% isatabbing
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	124	%\renewcommand{\isamarkupcmt}[1]%
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	125	%{\ifthenelse{\equal{TABSET}{#1}}{\=}%
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	126	% {\ifthenelse{\equal{TAB}{#1}}{\>}%
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	127	% {\ifthenelse{\equal{NEWLINE}{#1}}{\\}%
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	128	% {\ifthenelse{\equal{DOTS}{#1}}{\ldots}{\isastylecmt--- {#1}}}%
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	129	% }%
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	130	% }%
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	131	%}%
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	132
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	133
18 598409a21f4c added nasa talk Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	134
0 110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	135	\newenvironment{isatabbing}%
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	136	{\renewcommand{\isanewline}{\\}\begin{tabbing}}%
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	137	{\end{tabbing}}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	138
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	139	\begin{document}
18 598409a21f4c added nasa talk Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 0 diff changeset	140	\nocite{*}
0 110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	141	\input{session}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	142	\end{document}
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	143
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	144	%%% Local Variables:
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	145	%%% mode: latex
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	146	%%% TeX-master: t
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	147	%%% TeX-command-default: "Slides"
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	148	%%% TeX-view-style: (("." "kghostview --landscape --scale 0.45 --geometry 605x505 %f"))
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	149	%%% End:
110247f9d47e added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	150

author	zhangx
	Thu, 28 Jan 2016 21:14:17 +0800
changeset 90	ed938e2246b9
parent 20	b56616fd88dd
permissions	-rw-r--r--