From 8f47d9f3ca38a3fc2c3c462d1157866081102ce1 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 25 May 2020 15:24:20 +0200
Subject: 1. equality method now uses general elimination tactic. 2. New
 constant `` refers to rhs of equalities.

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

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

diff --git a/spartan/theories/Equivalence.thy b/spartan/theories/Equivalence.thy
index 73f1e0d..3415249 100644
--- a/spartan/theories/Equivalence.thy
+++ b/spartan/theories/Equivalence.thy
@@ -86,7 +86,7 @@ Lemma (derive) commute_homotopy:
   shows "(H x) \<bullet> g[p] = f[p] \<bullet> (H y)"
   \<comment> \<open>Need this assumption unfolded for typechecking:\<close>
   supply assms(8)[unfolded homotopy_def]
-  apply (equality \<open>p:_\<close>)
+  apply (eq p)
     focus vars x
       apply reduce
         \<comment> \<open>Here it would really be nice to have automation for transport and
@@ -366,7 +366,7 @@ Lemma
   assumes
     "A: U i" "B: U i" "p: A =\<^bsub>U i\<^esub> B"
   shows "A \<simeq> B"
-  by (equality \<open>p:_\<close>) (rule equivalence_refl)
+  by (eq p) (rule equivalence_refl)
 
 text \<open>
   The following proof is wordy because (1) the typechecker doesn't rewrite, and
@@ -383,7 +383,7 @@ Lemma (derive) id_imp_equiv:
   \<comment> \<open>Switch off auto-typechecking, which messes with universe levels\<close>
   supply [[auto_typechk=false]]
 
-    \<guillemotright> apply (equality \<open>p:_\<close>)
+    \<guillemotright> apply (eq p, typechk)
       \<^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])
-- 
cgit v1.2.3