# HG changeset patch
# User wenzelm
# Date 1451853934 -3600
# Node ID fefd79f6b232def7b188f1337229ac293c78cb35
# Parent  1ae53588dcbb6237faa785790c0485f8771c4b05
retain ASCII syntax for output, when HOL/Library/Lattice_Syntax is not present (amending e96292f32c3c);

diff -r 1ae53588dcbb -r fefd79f6b232 src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Sun Jan 03 21:31:57 2016 +0100
+++ b/src/HOL/Complete_Lattices.thy	Sun Jan 03 21:45:34 2016 +0100
@@ -91,6 +91,12 @@
   "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3SUP _./ _)" [0, 10] 10)
   "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3SUP _:_./ _)" [0, 0, 10] 10)
 
+syntax (output)
+  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3INF _./ _)" [0, 10] 10)
+  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3INF _:_./ _)" [0, 0, 10] 10)
+  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3SUP _./ _)" [0, 10] 10)
+  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3SUP _:_./ _)" [0, 0, 10] 10)
+
 syntax
   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
   "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
@@ -112,6 +118,7 @@
     Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPREMUM} @{syntax_const "_SUP"}]
 \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
 
+
 subsection \<open>Abstract complete lattices\<close>
 
 text \<open>A complete lattice always has a bottom and a top,