Binary file booklet.pdf has changed
--- a/booklet.tex Tue Aug 18 15:13:12 2015 +0800
+++ b/booklet.tex Tue Aug 18 15:24:17 2015 +0800
@@ -265,7 +265,7 @@
\begin{tabular}{l}
For the driver:\medskip\\
-司机师傅，请将我送往``{\bf 童卫路20号翰苑宾馆}''，其位置如地图中红色A点所示。\\
+司机师傅，请将我送到``{\bf 童卫路20号翰苑宾馆}''，其位置如地图中红色A点所示。\\
酒店电话：02584393962。谢谢！
\end{tabular}
@@ -564,8 +564,8 @@
\draw[line width=1mm,fill=gray!20] (0,2.0) rectangle (4,1.3);
\draw[line width=1mm,fill=gray!20] (4,2.0) rectangle (8,1.3);
- \draw (0,2.0) node[anchor=north west] {Info Desk 1st Floor};
- \draw (4,2.0) node[anchor=north west] {Info Desk 6th Floor};
+ \draw (0,2.0) node[anchor=north west] {Reg.~Desk 1st Floor};
+ \draw (4,2.0) node[anchor=north west] {Reg.~Desk 6th Floor};
\draw ( 3,0.8) node[anchor=north west]
{\small\begin{tabular}{@{}l}Re-\\cep-\\tion\\18:00\end{tabular}};
@@ -576,8 +576,8 @@
\end{tikzpicture}
\end{center}
-\noindent The Information Desk from Thursday (20th) to Sunday
-(23rd) will be on the 1st Floor next to the hotel registration
+\noindent Our registration desk from Thursday (20th) to Sunday
+(23rd) will be on the 1st Floor next to the hotel's registration
desk. From 24th, we will move the desk to the 6th floor where
the conference hall is. The Welcome Reception on Sunday will
also be on the 1st Floor. The programme of the talks is at the
@@ -641,8 +641,8 @@
There is a relatively large shopping area close to Xiamafang
Metro Station. There is also a wide selection of restaurants
in this area including Xingyuan's favourite restaurant for
-having lunch on workdays. It is called ?? and situated behind
-the KFC.
+having lunch on workdays. It is called Changjinglu
+(meaning giraffe) and situated behind the KFC.
\begin{center}
\includegraphics[scale=0.05]{travel_guide/rest.jpg}
@@ -654,32 +654,34 @@
at breakfast in the hotel). There is also pizza place in
case you must eat something different than Chinese.
-There is also a smaller shopping area in the ``middle'' of
-Tongwei road including some native restaurants, and also some
-restaurants on the opposite side of Houbiao\-ying Road. A smaller
-supermarket is at the end of Tongwei Road and a bigger one,
-called Suguo Community Store, in the Xiamafang area.
+There is also a smaller shopping area in the ``middle'' of
+Tongwei road including some native restaurants. Some more
+restaurants are on the opposite side of Houbiao\-ying Road.
+
+A smaller supermarket is at the end of Tongwei Road and a
+bigger one, called Suguo Community Store, in the Xiamafang
+area. For the latter, go down the steps in front of the KFC.
\end{itemize}
\section{Further Afield}
-If you take the very cheap metro, you are very quickly in the
-downtown area of Nanjing (see metro map in
-Fig.~\ref{metronanjing}).
+If you take the rather cheap and convenient metro, you are
+very quickly in the downtown area of Nanjing (see metro map in
+Fig.~\ref{metronanjing} in the previous section).
\begin{itemize}
\item\textbf{Shopping}\hspace{3mm}
-The most serious shopping malls in Nanjing are in the
-area around Xinjiekou and Daxinggong metro stations (on
-Line~2). Be aware that especially in multi-brand shopping
-malls the shopping goes like this: (1) You find something you
-like. (2) You agree the prize with the shop-assistant. (3) You
-get a piece of paper, which you need to take to a cashier
-nearby. (4) You pay there, get another piece of paper, which
-you take back to the shop-assistant, where you (5) receive your goods.
-Another ``quirk'' of shopping in China is that when the sale says,
-for example, ``80\% off'', it is actually 20\% off, meaning
-you pay only 80\% of the original price.
+The most serious shopping malls in Nanjing are in the area
+around Xinjiekou and Daxinggong metro stations (on Line~2). Be
+aware that especially in multi-brand shopping malls the
+shopping goes like this: (1) You find something you like. (2)
+You agree the prize with the shop-assistant. (3) You get a
+piece of paper, which you need to take to a cashier nearby.
+(4) You pay there, get another piece of paper, which you take
+back to the shop-assistant, where you finally (5) receive your
+goods. Another ``quirk'' of shopping in China is that when the
+sale says ``80\% off'', for example, it is actually 20\% off,
+meaning you pay only 80\% of the original price.
\item\textbf{Restaurants}\hspace{3mm}The most famous area
for restaurants in Nanjing is near the Confucius Temple, which
@@ -734,7 +736,7 @@
Tower in Chicago is 12th). A ticket for the observation
platform costs 66 RMB.\bigskip
-\noindent Nanjing Museum
+\noindent Nanjing Museum ??
\end{itemize}
@@ -765,6 +767,18 @@
around 21:30 and we should be back in the hotel by 23:00.
\end{itemize}
+\section{Restaurants}
+
+China is of course famous for its food and restaurants. Below
+we give an extremely selected list of a few restaurants in
+case you feel lost.
+
+\begin{itemize}
+\item\textbf{Quanjude / Beijing Duck}\hspace{3mm}Of course not
+native in Nanjing, but good anyway: If you want to try Bejing
+Duck, you should go to the Quanjude restaurant near the
+Xinjiekou Metro Station.
+\end{itemize}
\mbox{}\\[40mm]
\noindent The organising team wishes you a pleasant stay in
Binary file cert.pdf has changed
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/cert.tex Tue Aug 18 15:24:17 2015 +0800
@@ -0,0 +1,75 @@
+\documentclass[12pt, pagenumber=false, parskip=half,%
+ fromalign=right, fromphone=false,%
+ fromemail=false, fromurl=false,%
+ fromlogo=false, fromrule=false,%
+ backaddress=false, %
+ foldmarks=false]{scrlttr2}
+%%%%%%%%%%%%%%%%%%%%
+% fromalign = right (right, center) - Absenderfeld formatiert.
+% fromrule = afteraddress, false, aftername - ein Linie wird nach der Adresse gesetzt.
+% backaddress = true (false) - Setzen einer Rücksendeadresse für Fensterumschläge
+% fromphone = true - Setzen der Telefonnummer des Absenders
+% fromemail = true - Setzen der eMail-Adresse des Absenders
+% fromurl = true - Setzen einer Homepageadresse des Absenders
+% fromlogo = true - Absenderlogo (Firmenlogo) wird in den Brief eingefügt
+%%%%%%%%%%%%%%%%%%%%
+
+\usepackage{eurosym}
+\usepackage{textcomp}
+\usepackage{ulem}
+\usepackage{times}
+\usepackage[english]{babel}
+\usepackage[utf8]{inputenc}
+
+
+\renewcommand*{\raggedsignature}{\raggedright}
+\setkomavar{fromname}{Dr~Christian Urban}
+\setkomavar{fromaddress}{Department of Informatics\\
+ King's College London\\
+ Strand, London WC2R 2LS\\
+ United Kingdom}
+\setkomavar{signature}{Dr Christian Urban\\ co-chair of the ITP 2015 conference}
+
+
+\makeatletter
+\@addtoplength{firstheadvpos}{20mm}
+\makeatother
+
+\begin{document}
+\def\adrentry#1#2#3
+{\begin{letter}{\mbox{}}
+\opening{\bigskip\textbf{Certificate for the Registration Fee for the ITP 2015 Conference in Nanjing}}
+
+\bigskip
+This is to certify that
+
+\begin{center}
+\textbf{#1}
+\end{center}
+
+\noindent paid
+
+\begin{flushright}
+\begin{tabular}{l@{\hspace{5mm}}r}
+Total: & \uuline{#2}\\
+\end{tabular}
+\end{flushright}
+
+\noindent
+\if #30{for the International Conference on Interactive Theorem Proving, which took place
+from 24th until 27th of August in Nanjing, China.} \fi
+\if #31{for the International Conference on Interactive Theorem Proving and the Isabelle Tutorial,
+which both took place from 21st until 27th of August in Nanjing, China.} \fi
+\if #32{for the International Conference on Interactive Theorem Proving and the Coq Tutorial,
+which both took place from 24th until 29th of August in Nanjing, China.} \fi
+\if #33{for the International Conference on Interactive Theorem Proving, as well as the
+Isabelle and Coq Tutorials, which all took place from 21th until 29th of August in Nanjing, China.} \fi
+
+\bigskip\bigskip\bigskip
+
+\closing{\noindent{}Yours sincerely,\bigskip\mbox{}}
+\end{letter}
+
+}
+\input{participants.db}
+\end{document}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/participants.db Tue Aug 18 15:24:17 2015 +0800
@@ -0,0 +1,52 @@
+% 0 Main Conf
+% 1 Main Conf + Isa
+% 2 Main Conf + Coq
+% 3 Main Conf + Isa + Coq
+
+\adrentry{Sandrine Blazy}{\euro{}520}{2}
+\adrentry{David Pichardie}{\euro{}488}{0}
+\adrentry{Zoe Paraskevopoulou}{\euro{}510}{2}
+\adrentry{Arthur Chargu\'eraud}{\euro{}478}{0}
+\adrentry{Alexandre Mar\'echal}{\euro{}518.96}{1}
+\adrentry{Tobias Tebbi}{\euro{}488}{0}
+\adrentry{Andreas Lochbihler}{\$532}{0}
+\adrentry{Peter Lammich}{\euro{}520}{2}
+\adrentry{Tobias Nipkow}{\euro{}495.35}{0}
+\adrentry{Gert Smolka}{\euro{}569}{0}
+\adrentry{Lu\'is Cruz-Filipe}{\$533}{0}
+\adrentry{Reynald Affeldt }{\textyen{}69,615}{2}
+\adrentry{Rene Thiemann}{\euro{}475.16}{0}
+\adrentry{Sigurd Schneider}{\euro{}488}{0}
+\adrentry{Steven Sch\"afer}{\euro{}488}{0}
+\adrentry{Sylvain Boulm\'e}{\euro{}550}{3}
+\adrentry{Anthony Fox}{\pounds{}406}{0}
+\adrentry{Ond\v{r}ej Kun\v{c}ar}{\euro{}510}{2}
+\adrentry{Thomas Tuerk}{\euro{}478.35}{0}
+\adrentry{Abhishek Anand}{\$533}{0}
+\adrentry{Ramana Kumar}{\pounds{}359}{0}
+\adrentry{Prathamesh Turaga}{\$531}{0}
+\adrentry{Fabian Immler}{\euro{}520}{2}
+\adrentry{Stefan Hetzl}{\euro{}461}{0}
+\adrentry{Johannes Hoelzl}{\euro{}530}{2}
+\adrentry{Gregory Malecha}{\$533}{0}
+\adrentry{Pierre-Yves Strub}{\euro{}517.90}{2}
+\adrentry{Josef Urban}{\euro{}488}{0}
+\adrentry{Michael Norrish}{AU \$730}{0}
+\adrentry{Qinxiang Cao}{\$533}{0}
+
+
+%Petar Maksimovic 942 euro %% what shall we do
+%Pierre Wilke %% with these two
+
+%%%\adrentry{Hugo Herbelin}{3,500 RMB} % needs to pay with the hotel and show us the receipt
+
+%%\adrentry{Mariano Moscato}{\$563}{??} % not sure what he registered for
+
+%Cyril Cohen %% no money yet
+%Mohammad Abdulaziz
+%Qiaowen Jia(贾巧雯)
+%R\'egis Spadotti
+%Filip Sieczkowski
+
+%Peng Wu(吴鹏)
+%Xiaoyu Zhou(周晓宇)
\ No newline at end of file