diff options
author | Josh Chen | 2018-07-06 14:17:06 +0200 |
---|---|---|
committer | Josh Chen | 2018-07-06 14:17:06 +0200 |
commit | 1651beafbe7198a320fe87a926bf23e2ab1b784a (patch) | |
tree | 74272566201532dc9467eceb4fdbf4a99375b3b9 /Prod.thy | |
parent | 76deb7ae15fa00b5498ab43db020a0364499251e (diff) |
Remove extra attributes for elimination rules, unneeded for now.
Diffstat (limited to '')
-rw-r--r-- | Prod.thy | 3 |
1 files changed, 1 insertions, 2 deletions
@@ -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 |