diff options
| -rw-r--r-- | Equal.thy | 3 | ||||
| -rw-r--r-- | Prod.thy | 3 | ||||
| -rw-r--r-- | Sum.thy | 1 |
3 files changed, 2 insertions, 5 deletions
@@ -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 @@ -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 @@ -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 |