--- a/src/HOL/Lattices.thy Sat Nov 10 18:36:10 2007 +0100
+++ b/src/HOL/Lattices.thy Sat Nov 10 23:03:52 2007 +0100
@@ -12,9 +12,8 @@
subsection{* Lattices *}
notation
- less_eq (infix "\<sqsubseteq>" 50)
-and
- less (infix "\<sqsubset>" 50)
+ less_eq (infix "\<sqsubseteq>" 50) and
+ less (infix "\<sqsubset>" 50)
class lower_semilattice = order +
fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
@@ -30,6 +29,7 @@
class lattice = lower_semilattice + upper_semilattice
+
subsubsection{* Intro and elim rules*}
context lower_semilattice
@@ -398,13 +398,11 @@
by (simp add: Sup_insert_simp)
definition
- top :: 'a
-where
+ top :: 'a where
"top = \<Sqinter>{}"
definition
- bot :: 'a
-where
+ bot :: 'a where
"bot = \<Squnion>{}"
lemma top_greatest [simp]: "x \<le> top"
@@ -586,16 +584,11 @@
lemmas sup_aci = sup_ACI
no_notation
- less_eq (infix "\<sqsubseteq>" 50)
-and
- less (infix "\<sqsubset>" 50)
-and
- inf (infixl "\<sqinter>" 70)
-and
- sup (infixl "\<squnion>" 65)
-and
- Inf ("\<Sqinter>_" [900] 900)
-and
- Sup ("\<Squnion>_" [900] 900)
+ less_eq (infix "\<sqsubseteq>" 50) and
+ less (infix "\<sqsubset>" 50) and
+ inf (infixl "\<sqinter>" 70) and
+ sup (infixl "\<squnion>" 65) and
+ Inf ("\<Sqinter>_" [900] 900) and
+ Sup ("\<Squnion>_" [900] 900)
end
--- a/src/HOL/Nat.thy Sat Nov 10 18:36:10 2007 +0100
+++ b/src/HOL/Nat.thy Sat Nov 10 23:03:52 2007 +0100
@@ -1444,15 +1444,14 @@
begin
definition
- Nats :: "'a set"
-where
+ Nats :: "'a set" where
"Nats = range of_nat"
-end
-
notation (xsymbols)
Nats ("\<nat>")
+end
+
context semiring_1
begin
--- a/src/HOL/Subst/Subst.thy Sat Nov 10 18:36:10 2007 +0100
+++ b/src/HOL/Subst/Subst.thy Sat Nov 10 23:03:52 2007 +0100
@@ -22,14 +22,14 @@
definition
subst_eq :: "[('a*('a uterm)) list,('a*('a uterm)) list] => bool" (infixr "=$=" 52) where
"r =$= s \<longleftrightarrow> (\<forall>t. t \<lhd> r = t \<lhd> s)"
-notation
+notation (xsymbols)
subst_eq (infixr "\<doteq>" 52)
definition
comp :: "[('a*('a uterm)) list, ('a*('a uterm)) list] => ('a*('a uterm)) list"
(infixl "<>" 56) where
"al <> bl = alist_rec al bl (%x y xs g. (x,y \<lhd> bl)#g)"
-notation
+notation (xsymbols)
comp (infixl "\<lozenge>" 56)
definition
--- a/src/HOL/Word/BitSyntax.thy Sat Nov 10 18:36:10 2007 +0100
+++ b/src/HOL/Word/BitSyntax.thy Sat Nov 10 23:03:52 2007 +0100
@@ -25,15 +25,9 @@
*}
notation
- bitNOT ("NOT _" [70] 71)
-
-notation
- bitAND (infixr "AND" 64)
-
-notation
- bitOR (infixr "OR" 59)
-
-notation
+ bitNOT ("NOT _" [70] 71) and
+ bitAND (infixr "AND" 64) and
+ bitOR (infixr "OR" 59) and
bitXOR (infixr "XOR" 59)
text {*