From 720da0f918118388d114e09664b129d2b29be2b1 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Fri, 22 May 2020 15:43:14 +0200
Subject: some tweaks and comments, in preparation for general inductive type
 elimination

---
 spartan/theories/Equivalence.thy | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'spartan/theories/Equivalence.thy')

diff --git a/spartan/theories/Equivalence.thy b/spartan/theories/Equivalence.thy
index 44b77dd..97cd18d 100644
--- a/spartan/theories/Equivalence.thy
+++ b/spartan/theories/Equivalence.thy
@@ -197,7 +197,7 @@ Lemma (derive) funcomp_qinv:
   shows "qinv f \<rightarrow> qinv g \<rightarrow> qinv (g \<circ> f)"
   apply (intros, unfold qinv_def, elims)
   focus
-    premises hyps
+    prems prms
     vars _ _ finv _ ginv _ HfA HfB HgB HgC
 
     apply intro
@@ -246,7 +246,7 @@ Lemma (derive) biinv_imp_qinv:
   apply elims
 
   text \<open>Name the components:\<close>
-  focus premises vars _ _ _ g H1 h H2
+  focus prems vars _ _ _ g H1 h H2
   thm \<open>g:_\<close> \<open>h:_\<close> \<open>H1:_\<close> \<open>H2:_\<close>
 
   text \<open>
@@ -384,14 +384,14 @@ Lemma (derive) id_imp_equiv:
   supply [[auto_typechk=false]]
 
     \<guillemotright> apply (equality \<open>p:_\<close>)
-      \<^item> premises vars A B
+      \<^item> prems vars A B
         apply (rewrite at A in "A \<rightarrow> B" id_comp[symmetric])
         apply (rewrite at B in "_ \<rightarrow> B" id_comp[symmetric])
         apply (rule transport, rule U_in_U)
         apply (rule lift_universe_codomain, rule U_in_U)
         apply (typechk, rule U_in_U)
         done
-      \<^item> premises vars A
+      \<^item> prems vars A
         apply (subst transport_comp)
           \<^enum> by (rule U_in_U)
           \<^enum> by reduce (rule lift_universe)
-- 
cgit v1.2.3