aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2018-07-06 14:17:06 +0200
committerJosh Chen2018-07-06 14:17:06 +0200
commit1651beafbe7198a320fe87a926bf23e2ab1b784a (patch)
tree74272566201532dc9467eceb4fdbf4a99375b3b9
parent76deb7ae15fa00b5498ab43db020a0364499251e (diff)
Remove extra attributes for elimination rules, unneeded for now.
Diffstat (limited to '')
-rw-r--r--Equal.thy3
-rw-r--r--Prod.thy3
-rw-r--r--Sum.thy1
3 files changed, 2 insertions, 5 deletions
diff --git a/Equal.thy b/Equal.thy
index cb4d4f1..7732dd0 100644
--- a/Equal.thy
+++ b/Equal.thy
@@ -12,7 +12,7 @@ begin
axiomatization
Equal :: "[Term, Term, Term] \<Rightarrow> Term" and
refl :: "Term \<Rightarrow> Term" ("(refl'(_'))" 1000) and
- indEqual :: "[Term, [Term, Term] \<Rightarrow> Typefam, Term \<Rightarrow> Term, Term, Term, Term] \<Rightarrow> Term" ("(indEqual[_])")
+ indEqual :: "[Term, [Term, Term] \<Rightarrow> Typefam, Term \<Rightarrow> Term, Term, Term, Term] \<Rightarrow> Term" ("(1indEqual[_])")
section \<open>Syntax\<close>
@@ -53,7 +53,6 @@ and
\<rbrakk> \<Longrightarrow> indEqual[A] C f a a refl(a) \<equiv> f a"
lemmas Equal_rules [intro] = Equal_form Equal_intro Equal_elim Equal_comp
-lemmas Equal_elims [dest] = Equal_elim
lemmas Equal_form_conds [elim, wellform] = Equal_form_cond1 Equal_form_cond2 Equal_form_cond3
lemmas Equal_comps [comp] = Equal_comp
diff --git a/Prod.thy b/Prod.thy
index 9e1c1c3..544a719 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -20,7 +20,7 @@ section \<open>Syntax\<close>
syntax
"_PROD" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3\<Prod>_:_./ _)" 30)
- "_LAMBDA" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3\<^bold>\<lambda>_:_./ _)" 30)
+ "_LAMBDA" :: "[idt, Term, Term] \<Rightarrow> Term" ("(1\<^bold>\<lambda>_:_./ _)" 30)
"_PROD_ASCII" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3PROD _:_./ _)" 30)
"_LAMBDA_ASCII" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3%%_:_./ _)" 30)
@@ -59,7 +59,6 @@ This is what the additional formation rules \<open>Prod_form_cond1\<close> and \
text "The type rules should be able to be used as introduction and elimination rules by the standard reasoner:"
lemmas Prod_rules [intro] = Prod_form Prod_intro Prod_elim Prod_comp Prod_uniq
-lemmas Prod_elims [elim] = Prod_elim
lemmas Prod_form_conds [elim, wellform] = Prod_form_cond1 Prod_form_cond2
lemmas Prod_comps [comp] = Prod_comp Prod_uniq
diff --git a/Sum.thy b/Sum.thy
index 93fa791..fe38960 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -51,7 +51,6 @@ and
\<rbrakk> \<Longrightarrow> indSum[A,B] C f (a,b) \<equiv> f a b"
lemmas Sum_rules [intro] = Sum_form Sum_intro Sum_elim Sum_comp
-lemmas Sum_elims [dest] = Sum_elim \<comment> \<open>Declaring positively-presented dependent elimination rule as [dest] instead of [elim] arguably makes more sense.\<close>
lemmas Sum_form_conds [elim, wellform] = Sum_form_cond1 Sum_form_cond2
lemmas Sum_comps [comp] = Sum_comp