From a85c05db8b3952ae07a645abfdd8b5418808cfec Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Fri, 17 Aug 2018 13:39:56 +0200
Subject: Change unnecessary axiomatization to a definition

---
 Proj.thy | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Proj.thy')

diff --git a/Proj.thy b/Proj.thy
index 76f9f11..291113d 100644
--- a/Proj.thy
+++ b/Proj.thy
@@ -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."
 
-- 
cgit v1.2.3