From ad48f9176c58bdd4066389faa7a256fda8b58932 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sat, 23 Feb 2019 01:42:34 +0100
Subject: change mixfix pretty-printing indentation

---
 Prod.thy | 10 +++++-----
 Sum.thy  |  6 +++---
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/Prod.thy b/Prod.thy
index 059932c..afa543a 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -15,14 +15,14 @@ section \<open>Basic type definitions\<close>
 axiomatization
   Prod :: "[t, t \<Rightarrow> t] \<Rightarrow> t" and
   lam  :: "[t, t \<Rightarrow> t] \<Rightarrow> t" and
-  app  :: "[t, t] \<Rightarrow> t"  ("(1_ ` _)" [120, 121] 120)
+  app  :: "[t, t] \<Rightarrow> t"  ("(2_/ ` _)" [120, 121] 120)
   \<comment> \<open>Application should bind tighter than abstraction.\<close>
 
 syntax
-  "_Prod"  :: "[idt, t, t] \<Rightarrow> t"  ("(3\<Prod>'(_: _')./ _)" 30)
-  "_Prod'" :: "[idt, t, t] \<Rightarrow> t"  ("(3\<Prod>_: _./ _)" 30)
-  "_lam"   :: "[idt, t, t] \<Rightarrow> t"  ("(3\<lambda>'(_: _')./ _)" 30)
-  "_lam'"  :: "[idt, t, t] \<Rightarrow> t"  ("(3\<lambda>_: _./ _)" 30)
+  "_Prod"  :: "[idt, t, t] \<Rightarrow> t"  ("(2\<Prod>'(_: _')./ _)" 30)
+  "_Prod'" :: "[idt, t, t] \<Rightarrow> t"  ("(2\<Prod>_: _./ _)" 30)
+  "_lam"   :: "[idt, t, t] \<Rightarrow> t"  ("(2\<lambda>'(_: _')./ _)" 30)
+  "_lam'"  :: "[idt, t, t] \<Rightarrow> t"  ("(2\<lambda>_: _./ _)" 30)
 translations
   "\<Prod>(x: A). B" \<rightleftharpoons> "(CONST Prod) A (\<lambda>x. B)"
   "\<Prod>x: A. B" \<rightleftharpoons> "(CONST Prod) A (\<lambda>x. B)"
diff --git a/Sum.thy b/Sum.thy
index ee132b3..a1c0d34 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -11,12 +11,12 @@ begin
 
 axiomatization
   Sum    :: "[t, t \<Rightarrow> t] \<Rightarrow> t" and
-  pair   :: "[t, t] \<Rightarrow> t"  ("(1<_,/ _>)") and
+  pair   :: "[t, t] \<Rightarrow> t"  ("(2<_,/ _>)") and
   indSum :: "[t \<Rightarrow> t, [t, t] \<Rightarrow> t, t] \<Rightarrow> t"
 
 syntax
-  "_Sum"  :: "[idt, t, t] \<Rightarrow> t"  ("(3\<Sum>'(_: _')./ _)" 20)
-  "_Sum'" :: "[idt, t, t] \<Rightarrow> t"  ("(3\<Sum>_: _./ _)" 20)
+  "_Sum"  :: "[idt, t, t] \<Rightarrow> t"  ("(2\<Sum>'(_: _')./ _)" 20)
+  "_Sum'" :: "[idt, t, t] \<Rightarrow> t"  ("(2\<Sum>_: _./ _)" 20)
 translations
   "\<Sum>(x: A). B" \<rightleftharpoons> "(CONST Sum) A (\<lambda>x. B)"
   "\<Sum>x: A. B" \<rightleftharpoons> "(CONST Sum) A (\<lambda>x. B)"
-- 
cgit v1.2.3