From 575e98cac4871f0fdeefa0f5ac75bbba8103e82e Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 25 May 2020 16:01:18 +0200
Subject: use existing calculation infrastructure for sym and trans

---
 spartan/theories/Identity.thy | 15 +++------------
 1 file changed, 3 insertions(+), 12 deletions(-)

(limited to 'spartan/theories')

diff --git a/spartan/theories/Identity.thy b/spartan/theories/Identity.thy
index 1ab12ff..01bea46 100644
--- a/spartan/theories/Identity.thy
+++ b/spartan/theories/Identity.thy
@@ -139,18 +139,9 @@ in val _ = Context.>>
 end
 \<close>
 
-text \<open>Set up \<open>sym\<close> attribute for propositional equalities:\<close>
-
-ML \<open>
-structure Id_Sym_Attr = Sym_Attr (
-  struct
-    val name = "sym"
-    val symmetry_rule = @{thm pathinv[rotated 3]}
-  end
-)
-\<close>
-
-setup \<open>Id_Sym_Attr.setup\<close>
+lemmas
+  [sym] = pathinv[rotated 3] and
+  [trans] = pathcomp[rotated 4]
 
 
 section \<open>Basic propositional equalities\<close>
-- 
cgit v1.2.3