sen-material: slides/slides10.tex@6f884231ca57 (annotated)

88 a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1	\documentclass[dvipsnames,14pt,t]{beamer}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	2	\usepackage{proof}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	3	\usepackage{beamerthemeplainculight}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	4	\usepackage[T1]{fontenc}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	5	\usepackage[latin1]{inputenc}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	6	\usepackage{mathpartir}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	7	\usepackage{isabelle}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	8	\usepackage{isabellesym}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	9	\usepackage[absolute,overlay]{textpos}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	10	\usepackage{ifthen}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	11	\usepackage{tikz}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	12	\usepackage{courier}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	13	\usepackage{listings}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	14	\usetikzlibrary{arrows}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	15	\usetikzlibrary{positioning}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	16	\usetikzlibrary{calc}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	17	\usepackage{graphicx}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	18	\usetikzlibrary{shapes}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	19	\usetikzlibrary{shadows}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	20	\usetikzlibrary{plotmarks}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	21
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	22
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	23	\isabellestyle{rm}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	24	\renewcommand{\isastyle}{\rm}%
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	25	\renewcommand{\isastyleminor}{\rm}%
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	26	\renewcommand{\isastylescript}{\footnotesize\rm\slshape}%
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	27	\renewcommand{\isatagproof}{}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	28	\renewcommand{\endisatagproof}{}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	29	\renewcommand{\isamarkupcmt}[1]{#1}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	30
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	31	% Isabelle characters
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	32	\renewcommand{\isacharunderscore}{\_}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	33	\renewcommand{\isacharbar}{\isamath{\mid}}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	34	\renewcommand{\isasymiota}{}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	35	\renewcommand{\isacharbraceleft}{\{}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	36	\renewcommand{\isacharbraceright}{\}}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	37	\renewcommand{\isacharless}{$\langle$}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	38	\renewcommand{\isachargreater}{$\rangle$}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	39	\renewcommand{\isasymsharp}{\isamath{\#}}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	40	\renewcommand{\isasymdots}{\isamath{...}}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	41	\renewcommand{\isasymbullet}{\act}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	42
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	43	% beamer stuff
146 6f884231ca57 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 90 diff changeset	44	\renewcommand{\slidecaption}{APP 09, King's College London, 3 December 2013}
88 a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	45	\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	46	\newcommand{\bl}[1]{\textcolor{blue}{#1}}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	47
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	48	\begin{document}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	49
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	50	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	51	\mode<presentation>{
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	52	\begin{frame}<1>[t]
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	53	\frametitle{%
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	54	\begin{tabular}{@ {}c@ {}}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	55	\\
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	56	\LARGE Access Control and \\[-3mm]
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	57	\LARGE Privacy Policies (10)\\[-6mm]
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	58	\end{tabular}}\bigskip\bigskip\bigskip
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	59
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	60	%\begin{center}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	61	%\includegraphics[scale=1.3]{pics/barrier.jpg}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	62	%\end{center}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	63
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	64	\normalsize
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	65	\begin{center}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	66	\begin{tabular}{ll}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	67	Email: & christian.urban at kcl.ac.uk\\
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	68	Of$\!$fice: & S1.27 (1st floor Strand Building)\\
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	69	Slides: & KEATS (also homework is there)\\
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	70	\end{tabular}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	71	\end{center}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	72
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	73	\end{frame}}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	74	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	75
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	76
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	77	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	78	\mode<presentation>{
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	79	\begin{frame}[c]
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	80	\frametitle{Revision: Proofs}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	81
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	82	\begin{center}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	83	\includegraphics[scale=0.4]{pics/river-stones.jpg}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	84	\end{center}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	85
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	86	\begin{textblock}{5}(11.7,5)
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	87	goal
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	88	\end{textblock}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	89
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	90	\begin{textblock}{5}(11.7,14)
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	91	start
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	92	\end{textblock}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	93
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	94	\begin{textblock}{5}(0,7)
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	95	\begin{center}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	96	\bl{\infer[\small\textcolor{black}{\text{axiom}}]{\quad\vdash\quad}{}}\\[8mm]
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	97	\bl{\infer{\vdash}{\quad\vdash\quad}}\\[8mm]
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	98	\bl{\infer{\vdash}{\quad\vdash\qquad\vdash\quad}}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	99	\end{center}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	100	\end{textblock}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	101
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	102	\end{frame}}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	103	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	104
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	105	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	106	\mode<presentation>{
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	107	\begin{frame}[c]
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	108	\frametitle{Proof Example Proof}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	109
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	110	\begin{center}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	111	\bl{\infer{P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2 \wedge P\;\text{says}\;F_1}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	112	{\raisebox{2mm}{\text{\LARGE $?$}}}}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	113	\end{center}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	114
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	115
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	116	\end{frame}}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	117	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	118
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	119	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	120	\mode<presentation>{
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	121	\begin{frame}[c]
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	122	\frametitle{Proof Example Proof}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	123
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	124	\begin{tabular}{@{\hspace{-6mm}}l}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	125	\begin{minipage}{1.1\textwidth}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	126	We have (by axiom)
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	127
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	128	\begin{center}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	129	\begin{tabular}{@{}ll@{}}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	130	(1) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2$}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	131	\end{tabular}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	132	\end{center}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	133
89 be35ff24cccc added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 88 diff changeset	134	From (1) we get
88 a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	135
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	136	\begin{center}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	137	\begin{tabular}{@{}ll@{}}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	138	(2) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash P\;\text{says}\;F_1$}\\
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	139	(3) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2$}\\
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	140	\end{tabular}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	141	\end{center}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	142
89 be35ff24cccc added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 88 diff changeset	143	From (3) and (2) we get
88 a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	144
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	145	\begin{center}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	146	\begin{tabular}{@{}ll@{}}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	147	\bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2 \wedge P\;\text{says}\;F_1$}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	148	\end{tabular}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	149	\end{center}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	150
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	151	Done.
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	152	\end{minipage}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	153	\end{tabular}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	154
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	155	\end{frame}}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	156	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	157
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	158
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	159	\end{document}
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	160
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	161	%%% Local Variables:
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	162	%%% mode: latex
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	163	%%% TeX-master: t
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	164	%%% End:
a30f60a08939 added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	165

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Tue, 03 Dec 2013 03:20:42 +0000
changeset 146	6f884231ca57
parent 90	d1d07f05325a
child 152	0c62ec6dc691
permissions	-rw-r--r--