src/HOL/Library/Option_ord.thy
changeset 61955 e96292f32c3c
parent 60679 ade12ef2773c
child 62343 24106dc44def
     1.1 --- a/src/HOL/Library/Option_ord.thy	Mon Dec 28 19:23:15 2015 +0100
     1.2 +++ b/src/HOL/Library/Option_ord.thy	Mon Dec 28 21:47:32 2015 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4    Inf  ("\<Sqinter>_" [900] 900) and
     1.5    Sup  ("\<Squnion>_" [900] 900)
     1.6  
     1.7 -syntax (xsymbols)
     1.8 +syntax
     1.9    "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
    1.10    "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
    1.11    "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
    1.12 @@ -348,7 +348,7 @@
    1.13    Inf  ("\<Sqinter>_" [900] 900) and
    1.14    Sup  ("\<Squnion>_" [900] 900)
    1.15  
    1.16 -no_syntax (xsymbols)
    1.17 +no_syntax
    1.18    "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
    1.19    "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
    1.20    "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)