explicit remove of lattice notation
authorhaftmann
Fri Feb 24 08:49:36 2012 +0100 (2012-02-24)
changeset 466370bd7c16a4200
parent 46636 353731f11559
child 46638 fc315796794e
explicit remove of lattice notation
src/HOL/Relation.thy
     1.1 --- a/src/HOL/Relation.thy	Fri Feb 24 07:30:24 2012 +0100
     1.2 +++ b/src/HOL/Relation.thy	Fri Feb 24 08:49:36 2012 +0100
     1.3 @@ -931,4 +931,18 @@
     1.4    obtains "r x z"
     1.5    using assms by (auto dest: transD simp add: transp_def)
     1.6  
     1.7 +no_notation
     1.8 +  bot ("\<bottom>") and
     1.9 +  top ("\<top>") and
    1.10 +  inf (infixl "\<sqinter>" 70) and
    1.11 +  sup (infixl "\<squnion>" 65) and
    1.12 +  Inf ("\<Sqinter>_" [900] 900) and
    1.13 +  Sup ("\<Squnion>_" [900] 900)
    1.14 +
    1.15 +no_syntax (xsymbols)
    1.16 +  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
    1.17 +  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
    1.18 +  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
    1.19 +  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
    1.20 +
    1.21  end