From b0ba102b783418560f9b7b15239681b11ea4c877 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 26 May 2020 16:50:35 +0200
Subject: new material

---
 hott/Nat.thy | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'hott/Nat.thy')

diff --git a/hott/Nat.thy b/hott/Nat.thy
index d54ea7b..c36154e 100644
--- a/hott/Nat.thy
+++ b/hott/Nat.thy
@@ -44,7 +44,7 @@ lemmas
 
 text \<open>Non-dependent recursion\<close>
 
-abbreviation "NatRec C \<equiv> NatInd (K C)"
+abbreviation "NatRec C \<equiv> NatInd (\<lambda>_. C)"
 
 
 section \<open>Basic arithmetic\<close>
@@ -100,10 +100,10 @@ Lemma (derive) add_comm:
   shows "m + n = n + m"
   apply (elim m)
     \<guillemotright> by (reduce; rule add_zero[symmetric])
-    \<guillemotright> prems prms vars m ih
+    \<guillemotright> prems vars m ih
       proof reduce
         have "suc (m + n) = suc (n + m)" by (eq ih) intro
-        also have "'' = n + suc m" by (rule add_suc[symmetric])
+        also have ".. = n + suc m" by (rule add_suc[symmetric])
         finally show "suc (m + n) = n + suc m" by this
       qed
   done
-- 
cgit v1.2.3