change mixfix pretty-printing indentation

1 files changed, 5 insertions, 5 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)"