From 5161a0356d8752f3b1b4f4385e799bca92718814 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sun, 17 Jun 2018 00:48:01 +0200
Subject: Decided on a new proper scheme for type rules using the idea of
 implicit well-formed contexts and guaranteed conclusion well-formedness.
 Product type rules now follow this scheme.

---
 Prod.thy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Prod.thy')

diff --git a/Prod.thy b/Prod.thy
index 113998e..7cce7f0 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -33,7 +33,7 @@ translations
 axiomatization where
   Prod_form [intro]: "\<And>A B. \<lbrakk>A : U; B : A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Prod>x:A. B x : U"
 and
-  Prod_intro [intro]: "\<And>A B b. (\<And>x. x : A \<Longrightarrow> b x : B x) \<Longrightarrow> \<^bold>\<lambda>x:A. b x : \<Prod>x:A. B x"
+  Prod_intro [intro]: "\<And>A B b. \<lbrakk>A : U; \<And>x. x : A \<Longrightarrow> b x : B x\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x:A. b x : \<Prod>x:A. B x"
 and
   Prod_elim [elim]: "\<And>A B f a. \<lbrakk>f : \<Prod>x:A. B x; a : A\<rbrakk> \<Longrightarrow> f`a : B a"
 and
-- 
cgit v1.2.3