From 12eed8685674b7d5ff7bc45a44a061e01f99ce5f Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 21 Jul 2020 02:09:44 +0200
Subject: 1. Type-checking/inference now more principled, and the
 implementation is better. 2. Changed most tactics to context tactics.

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

(limited to 'hott/More_Nat.thy')

diff --git a/hott/More_Nat.thy b/hott/More_Nat.thy
index 8177170..59c8d54 100644
--- a/hott/More_Nat.thy
+++ b/hott/More_Nat.thy
@@ -15,15 +15,15 @@ Lemma (derive) eq: shows "Nat \<rightarrow> Nat \<rightarrow> U O"
     apply intro focus vars n apply elim
       \<guillemotright> by (rule TopF) \<comment> \<open>n \<equiv> 0\<close>
       \<guillemotright> by (rule BotF) \<comment> \<open>n \<equiv> suc _\<close>
-      \<guillemotright> by (rule U_in_U)
+      \<guillemotright> by (rule Ui_in_USi)
     done
     \<comment> \<open>m \<equiv> suc k\<close>
     apply intro focus vars k k_eq n apply (elim n)
       \<guillemotright> by (rule BotF) \<comment> \<open>n \<equiv> 0\<close>
       \<guillemotright> prems vars l proof - show "k_eq l: U O" by typechk qed
-      \<guillemotright> by (rule U_in_U)
+      \<guillemotright> by (rule Ui_in_USi)
     done
-    by (rule U_in_U)
+    by (rule Ui_in_USi)
   done
 
 text \<open>
-- 
cgit v1.2.3