# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1484552422 -32400
# Node ID 2f944ab2f5f665f040f0fc3dbe339e22e1fb8c27
# Parent  f6931d3d59c07eb3bc379afe36040c5b4f41a9a7
Mini fixes

diff -r f6931d3d59c0 -r 2f944ab2f5f6 paper/abstract.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/abstract.tex	Mon Jan 16 16:40:22 2017 +0900
@@ -0,0 +1,3 @@
+\begin{abstract}
+
+\end{abstract}
diff -r f6931d3d59c0 -r 2f944ab2f5f6 paper/abstract_eng.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/abstract_eng.tex	Mon Jan 16 16:40:22 2017 +0900
@@ -0,0 +1,3 @@
+\begin{abstract_eng}
+    
+\end{abstract_eng}
diff -r f6931d3d59c0 -r 2f944ab2f5f6 paper/atton-master.tex
--- a/paper/atton-master.tex	Mon Jan 16 16:28:42 2017 +0900
+++ b/paper/atton-master.tex	Mon Jan 16 16:40:22 2017 +0900
@@ -11,6 +11,7 @@
 \usepackage{listings}
 \usepackage{bussproofs}
 \usepackage{amssymb}
+\usepackage{amsmath}
 \usepackage[utf8]{inputenc}
 
 %\input{dummy.tex} %% font
@@ -74,8 +75,8 @@
 \makecommission
 
 %要旨
-% \input{abstract.tex}
-% \input{abstract_eng.tex}
+\input{abstract.tex}
+\input{abstract_eng.tex}
 
 %目次
 \tableofcontents
@@ -106,7 +107,7 @@
 \section{部分型と Continuation based C}
 
 \chapter{証明支援系言語 Agda による証明手法}
-\section{TODO: Agda tutorial 的なもの}
+\section{依存型を持つ証明支援系言語 Agda}
 \section{Natural Deduction}
 \section{Curry-Howard Isomorphism}
 \section{Reasoning}