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_List.thy | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'hott/More_List.thy')

diff --git a/hott/More_List.thy b/hott/More_List.thy
index 460dc7b..1b8034f 100644
--- a/hott/More_List.thy
+++ b/hott/More_List.thy
@@ -10,8 +10,8 @@ section \<open>Length\<close>
 definition [implicit]: "len \<equiv> ListRec ? Nat 0 (fn _ _ rec. suc rec)"
 
 experiment begin
-  Lemma "len [] \<equiv> ?n" by (subst comps)+
-  Lemma "len [0, suc 0, suc (suc 0)] \<equiv> ?n" by (subst comps)+
+  Lemma "len [] \<equiv> ?n" by (subst comp)+
+  Lemma "len [0, suc 0, suc (suc 0)] \<equiv> ?n" by (subst comp)+
 end
 
 
-- 
cgit v1.2.3

