tuned syntax declarations; tuned structure
authorhaftmann
Sun Feb 26 20:10:14 2012 +0100 (2012-02-26)
changeset 4669172d81e789106
parent 46690 07f9732804ad
child 46692 1f8b766224f6
tuned syntax declarations; tuned structure
src/HOL/Complete_Lattices.thy
src/HOL/Lattices.thy
src/HOL/Orderings.thy
src/HOL/Plain.thy
src/HOL/Relation.thy
     1.1 --- a/src/HOL/Complete_Lattices.thy	Sun Feb 26 20:08:12 2012 +0100
     1.2 +++ b/src/HOL/Complete_Lattices.thy	Sun Feb 26 20:10:14 2012 +0100
     1.3 @@ -8,11 +8,7 @@
     1.4  
     1.5  notation
     1.6    less_eq (infix "\<sqsubseteq>" 50) and
     1.7 -  less (infix "\<sqsubset>" 50) and
     1.8 -  inf (infixl "\<sqinter>" 70) and
     1.9 -  sup (infixl "\<squnion>" 65) and
    1.10 -  top ("\<top>") and
    1.11 -  bot ("\<bottom>")
    1.12 +  less (infix "\<sqsubset>" 50)
    1.13  
    1.14  
    1.15  subsection {* Syntactic infimum and supremum operations *}
    1.16 @@ -23,6 +19,7 @@
    1.17  class Sup =
    1.18    fixes Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
    1.19  
    1.20 +
    1.21  subsection {* Abstract complete lattices *}
    1.22  
    1.23  class complete_lattice = bounded_lattice + Inf + Sup +
    1.24 @@ -1214,14 +1211,8 @@
    1.25  text {* Finally *}
    1.26  
    1.27  no_notation
    1.28 -  less_eq  (infix "\<sqsubseteq>" 50) and
    1.29 -  less (infix "\<sqsubset>" 50) and
    1.30 -  bot ("\<bottom>") and
    1.31 -  top ("\<top>") and
    1.32 -  inf  (infixl "\<sqinter>" 70) and
    1.33 -  sup  (infixl "\<squnion>" 65) and
    1.34 -  Inf  ("\<Sqinter>_" [900] 900) and
    1.35 -  Sup  ("\<Squnion>_" [900] 900)
    1.36 +  less_eq (infix "\<sqsubseteq>" 50) and
    1.37 +  less (infix "\<sqsubset>" 50)
    1.38  
    1.39  no_syntax (xsymbols)
    1.40    "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
     2.1 --- a/src/HOL/Lattices.thy	Sun Feb 26 20:08:12 2012 +0100
     2.2 +++ b/src/HOL/Lattices.thy	Sun Feb 26 20:10:14 2012 +0100
     2.3 @@ -43,13 +43,7 @@
     2.4  end
     2.5  
     2.6  
     2.7 -subsection {* Concrete lattices *}
     2.8 -
     2.9 -notation
    2.10 -  less_eq  (infix "\<sqsubseteq>" 50) and
    2.11 -  less  (infix "\<sqsubset>" 50) and
    2.12 -  bot ("\<bottom>") and
    2.13 -  top ("\<top>")
    2.14 +subsection {* Syntactic infimum and supremum operations *}
    2.15  
    2.16  class inf =
    2.17    fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
    2.18 @@ -57,6 +51,13 @@
    2.19  class sup = 
    2.20    fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
    2.21  
    2.22 +
    2.23 +subsection {* Concrete lattices *}
    2.24 +
    2.25 +notation
    2.26 +  less_eq  (infix "\<sqsubseteq>" 50) and
    2.27 +  less  (infix "\<sqsubset>" 50)
    2.28 +
    2.29  class semilattice_inf =  order + inf +
    2.30    assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x"
    2.31    and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
    2.32 @@ -759,12 +760,8 @@
    2.33  
    2.34  
    2.35  no_notation
    2.36 -  less_eq  (infix "\<sqsubseteq>" 50) and
    2.37 -  less (infix "\<sqsubset>" 50) and
    2.38 -  inf  (infixl "\<sqinter>" 70) and
    2.39 -  sup  (infixl "\<squnion>" 65) and
    2.40 -  top ("\<top>") and
    2.41 -  bot ("\<bottom>")
    2.42 +  less_eq (infix "\<sqsubseteq>" 50) and
    2.43 +  less (infix "\<sqsubset>" 50)
    2.44  
    2.45  end
    2.46  
     3.1 --- a/src/HOL/Orderings.thy	Sun Feb 26 20:08:12 2012 +0100
     3.2 +++ b/src/HOL/Orderings.thy	Sun Feb 26 20:10:14 2012 +0100
     3.3 @@ -1426,8 +1426,4 @@
     3.4  lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
     3.5  lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
     3.6  
     3.7 -no_notation
     3.8 -  top ("\<top>") and
     3.9 -  bot ("\<bottom>")
    3.10 -
    3.11  end
     4.1 --- a/src/HOL/Plain.thy	Sun Feb 26 20:08:12 2012 +0100
     4.2 +++ b/src/HOL/Plain.thy	Sun Feb 26 20:10:14 2012 +0100
     4.3 @@ -9,4 +9,18 @@
     4.4    include @{text Hilbert_Choice}.
     4.5  *}
     4.6  
     4.7 +no_notation
     4.8 +  bot ("\<bottom>") and
     4.9 +  top ("\<top>") and
    4.10 +  inf (infixl "\<sqinter>" 70) and
    4.11 +  sup (infixl "\<squnion>" 65) and
    4.12 +  Inf ("\<Sqinter>_" [900] 900) and
    4.13 +  Sup ("\<Squnion>_" [900] 900)
    4.14 +
    4.15 +no_syntax (xsymbols)
    4.16 +  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
    4.17 +  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
    4.18 +  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
    4.19 +  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
    4.20 +
    4.21  end
     5.1 --- a/src/HOL/Relation.thy	Sun Feb 26 20:08:12 2012 +0100
     5.2 +++ b/src/HOL/Relation.thy	Sun Feb 26 20:10:14 2012 +0100
     5.3 @@ -939,19 +939,5 @@
     5.4    obtains "r x z"
     5.5    using assms by (auto dest: transD simp add: transp_def)
     5.6  
     5.7 -no_notation
     5.8 -  bot ("\<bottom>") and
     5.9 -  top ("\<top>") and
    5.10 -  inf (infixl "\<sqinter>" 70) and
    5.11 -  sup (infixl "\<squnion>" 65) and
    5.12 -  Inf ("\<Sqinter>_" [900] 900) and
    5.13 -  Sup ("\<Squnion>_" [900] 900)
    5.14 -
    5.15 -no_syntax (xsymbols)
    5.16 -  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
    5.17 -  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
    5.18 -  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
    5.19 -  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
    5.20 -
    5.21  end
    5.22