# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1487056708 -32400
# Node ID 7ab9767dc9f9283f0d948c810daa32e0e4483002
# Parent  81978a9122f0d82bdff6b02971406230cd2a1072
Update slide

diff -r 81978a9122f0 -r 7ab9767dc9f9 presentation/slide.html
--- a/presentation/slide.html	Tue Feb 14 16:09:01 2017 +0900
+++ b/presentation/slide.html	Tue Feb 14 16:18:28 2017 +0900
@@ -86,7 +86,7 @@
 <!-- === begin markdown block ===
 
       generated by markdown/1.2.0 on Ruby 2.3.3 (2016-11-21) [x86_64-darwin16]
-                on 2017-02-14 16:08:41 +0900 with Markdown engine kramdown (1.13.0)
+                on 2017-02-14 16:17:51 +0900 with Markdown engine kramdown (1.13.0)
                   using options {}
   -->
 
@@ -443,11 +443,6 @@
 <!-- _S9SLIDE_ -->
 <h1 id="agda-">Agda における証明</h1>
 <ul>
-  <li>Curry-Howard Isomorphism による型付きラムダ計算と自然演繹の対応
-    <ul>
-      <li>自然演繹: 命題、ならば、かつ、または、で構成される証明システム</li>
-    </ul>
-  </li>
   <li>論理式は型に相当して、証明はその値の導出</li>
   <li>三段論法の証明は以下のようになる
     <ul>
diff -r 81978a9122f0 -r 7ab9767dc9f9 presentation/slide.md
--- a/presentation/slide.md	Tue Feb 14 16:09:01 2017 +0900
+++ b/presentation/slide.md	Tue Feb 14 16:18:28 2017 +0900
@@ -189,8 +189,6 @@
 * Agda 上に CbC を定義することで形式的な定義を得る
 
 # Agda における証明
-* Curry-Howard Isomorphism による型付きラムダ計算と自然演繹の対応
-    * 自然演繹: 命題、ならば、かつ、または、で構成される証明システム
 * 論理式は型に相当して、証明はその値の導出
 * 三段論法の証明は以下のようになる
     * 「((A ならば B) かつ (B ならば C)) ならば (A ならば C)
diff -r 81978a9122f0 -r 7ab9767dc9f9 presentation/slide.pdf.html
--- a/presentation/slide.pdf.html	Tue Feb 14 16:09:01 2017 +0900
+++ b/presentation/slide.pdf.html	Tue Feb 14 16:18:28 2017 +0900
@@ -70,7 +70,7 @@
 <!-- === begin markdown block ===
 
       generated by markdown/1.2.0 on Ruby 2.3.3 (2016-11-21) [x86_64-darwin16]
-                on 2017-02-14 16:08:41 +0900 with Markdown engine kramdown (1.13.0)
+                on 2017-02-14 16:17:51 +0900 with Markdown engine kramdown (1.13.0)
                   using options {}
   -->
 
@@ -427,11 +427,6 @@
 <!-- _S9SLIDE_ -->
 <h1 id="agda-">Agda における証明</h1>
 <ul>
-  <li>Curry-Howard Isomorphism による型付きラムダ計算と自然演繹の対応
-    <ul>
-      <li>自然演繹: 命題、ならば、かつ、または、で構成される証明システム</li>
-    </ul>
-  </li>
   <li>論理式は型に相当して、証明はその値の導出</li>
   <li>三段論法の証明は以下のようになる
     <ul>