From 17b9392e7f5d568f6bfb5b0d552866e18c118762 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Thu, 28 May 2020 16:00:31 +0200
Subject: notation

---
 spartan/core/Spartan.thy | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy
index b0fec5a..3d59464 100644
--- a/spartan/core/Spartan.thy
+++ b/spartan/core/Spartan.thy
@@ -115,6 +115,9 @@ translations "\<Sum>x: A. B" \<rightleftharpoons> "CONST Sig A (\<lambda>x. B)"
 abbreviation Prod (infixl "\<times>" 60)
   where "A \<times> B \<equiv> \<Sum>_: A. B"
 
+abbreviation "and" (infixl "\<and>" 60)
+  where "A \<and> B \<equiv> A \<times> B"
+
 axiomatization where
   SigF: "\<lbrakk>\<And>x. x: A \<Longrightarrow> B x: U i; A: U i\<rbrakk> \<Longrightarrow> \<Sum>x: A. B x: U i" and
 
-- 
cgit v1.2.3