diff options
| author | Josh Chen | 2018-08-17 13:39:56 +0200 |
|---|---|---|
| committer | Josh Chen | 2018-08-17 13:39:56 +0200 |
| commit | a85c05db8b3952ae07a645abfdd8b5418808cfec (patch) | |
| tree | 181122ca233d1ea25e14ca1bf22ad63388ed85a0 | |
| parent | 10757b7f628655f962b2dd1c7849c75098320ed1 (diff) | |
Change unnecessary axiomatization to a definition
| -rw-r--r-- | Proj.thy | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -13,8 +13,8 @@ theory Proj begin -axiomatization fst :: "Term \<Rightarrow> Term" where fst_def: "fst \<equiv> \<lambda>p. ind\<^sub>\<Sum>(\<lambda>x y. x)(p)" -axiomatization snd :: "Term \<Rightarrow> Term" where snd_def: "snd \<equiv> \<lambda>p. ind\<^sub>\<Sum>(\<lambda>x y. y)(p)" +definition fst :: "Term \<Rightarrow> Term" where "fst(p) \<equiv> ind\<^sub>\<Sum> (\<lambda>x y. x) p" +definition snd :: "Term \<Rightarrow> Term" where "snd(p) \<equiv> ind\<^sub>\<Sum> (\<lambda>x y. y) p" text "Typing judgments and computation rules for the dependent and non-dependent projection functions." |