From 76deb7ae15fa00b5498ab43db020a0364499251e Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Fri, 6 Jul 2018 10:48:41 +0200
Subject: Added attributes to type elimination rules, not sure if these will
 actually be needed or useful later. Added [comp] attribute to be used by
 simplification met methods.

---
 EqualProps.thy | 21 ---------------------
 1 file changed, 21 deletions(-)

(limited to 'EqualProps.thy')

diff --git a/EqualProps.thy b/EqualProps.thy
index 8960a90..2807587 100644
--- a/EqualProps.thy
+++ b/EqualProps.thy
@@ -66,27 +66,6 @@ lemma compose_comp:
   assumes "a : A"
   shows "compose[A,a,a,a]`refl(a)`refl(a) \<equiv> refl(a)"
 
-proof (unfold rcompose_def)
-  show "(\<^bold>\<lambda>p:a =[A] a.
-        lambda (a =[A] a)
-         (op `
-           ((\<^bold>\<lambda>x:A.
-                \<^bold>\<lambda>y:A.
-                   lambda (x =[A] y)
-                    (indEqual[A]
-                      (\<lambda>x y _. \<Prod>z:A. y =[A] z \<rightarrow> x =[A] z)
-                      (\<lambda>x. \<^bold>\<lambda>z:A.
- lambda (x =[A] z)
-  (indEqual[A] (\<lambda>x z _. x =[A] z) refl x z))
-                      x y)) `
-            a `
-            a `
-            p `
-            a))) `
-    refl(a) `
-    refl(a) \<equiv>
-    refl(a)"
-
 sorry \<comment> \<open>Long and tedious proof if the Simplifier is not set up.\<close>
 
 
-- 
cgit v1.2.3