# HG changeset patch
# User haftmann
# Date 1266916275 -3600
# Node ID d57da4abb47d34f3d1573cea906ffe3421c73e4d
# Parent  870dfea4f9c0775cc7918779d1f891fda20cce50
dropped axclass; dropped Id

diff -r 870dfea4f9c0 -r d57da4abb47d src/HOL/Isar_Examples/Group.thy
--- a/src/HOL/Isar_Examples/Group.thy	Tue Feb 23 10:11:15 2010 +0100
+++ b/src/HOL/Isar_Examples/Group.thy	Tue Feb 23 10:11:15 2010 +0100
@@ -17,15 +17,12 @@
  $\idt{times}$ is provided by the basic HOL theory.
 *}
 
-consts
-  one :: "'a"
-  inverse :: "'a => 'a"
+notation Groups.one ("one")
 
-axclass
-  group < times
-  group_assoc:         "(x * y) * z = x * (y * z)"
-  group_left_one:      "one * x = x"
-  group_left_inverse:  "inverse x * x = one"
+class group = times + one + inverse +
+  assumes group_assoc:         "(x * y) * z = x * (y * z)"
+  assumes group_left_one:      "one * x = x"
+  assumes group_left_inverse:  "inverse x * x = one"
 
 text {*
  The group axioms only state the properties of left one and inverse,
@@ -144,10 +141,10 @@
  \idt{one} :: \alpha)$ are defined like this.
 *}
 
-axclass monoid < times
-  monoid_assoc:       "(x * y) * z = x * (y * z)"
-  monoid_left_one:   "one * x = x"
-  monoid_right_one:  "x * one = x"
+class monoid = times + one +
+  assumes monoid_assoc:       "(x * y) * z = x * (y * z)"
+  assumes monoid_left_one:   "one * x = x"
+  assumes monoid_right_one:  "x * one = x"
 
 text {*
  Groups are \emph{not} yet monoids directly from the definition.  For
diff -r 870dfea4f9c0 -r d57da4abb47d src/HOL/Lattice/Bounds.thy
--- a/src/HOL/Lattice/Bounds.thy	Tue Feb 23 10:11:15 2010 +0100
+++ b/src/HOL/Lattice/Bounds.thy	Tue Feb 23 10:11:15 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Lattice/Bounds.thy
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 *)
 
diff -r 870dfea4f9c0 -r d57da4abb47d src/HOL/Lattice/CompleteLattice.thy
--- a/src/HOL/Lattice/CompleteLattice.thy	Tue Feb 23 10:11:15 2010 +0100
+++ b/src/HOL/Lattice/CompleteLattice.thy	Tue Feb 23 10:11:15 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Lattice/CompleteLattice.thy
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 *)
 
@@ -16,8 +15,8 @@
   bounds (see \S\ref{sec:connect-bounds}).
 *}
 
-axclass complete_lattice \<subseteq> partial_order
-  ex_Inf: "\<exists>inf. is_Inf A inf"
+class complete_lattice =
+  assumes ex_Inf: "\<exists>inf. is_Inf A inf"
 
 theorem ex_Sup: "\<exists>sup::'a::complete_lattice. is_Sup A sup"
 proof -
diff -r 870dfea4f9c0 -r d57da4abb47d src/HOL/Lattice/Lattice.thy
--- a/src/HOL/Lattice/Lattice.thy	Tue Feb 23 10:11:15 2010 +0100
+++ b/src/HOL/Lattice/Lattice.thy	Tue Feb 23 10:11:15 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Lattice/Lattice.thy
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 *)
 
@@ -15,9 +14,9 @@
   as well).
 *}
 
-axclass lattice \<subseteq> partial_order
-  ex_inf: "\<exists>inf. is_inf x y inf"
-  ex_sup: "\<exists>sup. is_sup x y sup"
+class lattice =
+  assumes ex_inf: "\<exists>inf. is_inf x y inf"
+  assumes ex_sup: "\<exists>sup. is_sup x y sup"
 
 text {*
   The @{text \<sqinter>} (meet) and @{text \<squnion>} (join) operations select such
diff -r 870dfea4f9c0 -r d57da4abb47d src/HOL/Lattice/Orders.thy
--- a/src/HOL/Lattice/Orders.thy	Tue Feb 23 10:11:15 2010 +0100
+++ b/src/HOL/Lattice/Orders.thy	Tue Feb 23 10:11:15 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Lattice/Orders.thy
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 *)
 
@@ -18,21 +17,21 @@
   required to be related (in either direction).
 *}
 
-axclass leq < type
-consts
-  leq :: "'a::leq \<Rightarrow> 'a \<Rightarrow> bool"  (infixl "[=" 50)
+class leq =
+  fixes leq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infixl "[=" 50)
+
 notation (xsymbols)
   leq  (infixl "\<sqsubseteq>" 50)
 
-axclass quasi_order < leq
-  leq_refl [intro?]: "x \<sqsubseteq> x"
-  leq_trans [trans]: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
+class quasi_order = leq +
+  assumes leq_refl [intro?]: "x \<sqsubseteq> x"
+  assumes leq_trans [trans]: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
 
-axclass partial_order < quasi_order
-  leq_antisym [trans]: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
+class partial_order = quasi_order +
+  assumes leq_antisym [trans]: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
 
-axclass linear_order < partial_order
-  leq_linear: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
+class linear_order = partial_order +
+  assumes leq_linear: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
 
 lemma linear_order_cases:
     "((x::'a::linear_order) \<sqsubseteq> y \<Longrightarrow> C) \<Longrightarrow> (y \<sqsubseteq> x \<Longrightarrow> C) \<Longrightarrow> C"
@@ -54,11 +53,16 @@
 primrec
   undual_dual: "undual (dual x) = x"
 
-instance dual :: (leq) leq ..
+instantiation dual :: (leq) leq
+begin
 
-defs (overloaded)
+definition
   leq_dual_def: "x' \<sqsubseteq> y' \<equiv> undual y' \<sqsubseteq> undual x'"
 
+instance ..
+
+end
+
 lemma undual_leq [iff?]: "(undual x' \<sqsubseteq> undual y') = (y' \<sqsubseteq> x')"
   by (simp add: leq_dual_def)
 
@@ -192,11 +196,16 @@
   \emph{not} be linear in general.
 *}
 
-instance * :: (leq, leq) leq ..
+instantiation * :: (leq, leq) leq
+begin
 
-defs (overloaded)
+definition
   leq_prod_def: "p \<sqsubseteq> q \<equiv> fst p \<sqsubseteq> fst q \<and> snd p \<sqsubseteq> snd q"
 
+instance ..
+
+end
+
 lemma leq_prodI [intro?]:
     "fst p \<sqsubseteq> fst q \<Longrightarrow> snd p \<sqsubseteq> snd q \<Longrightarrow> p \<sqsubseteq> q"
   by (unfold leq_prod_def) blast
@@ -249,11 +258,16 @@
   orders need \emph{not} be linear in general.
 *}
 
-instance "fun" :: (type, leq) leq ..
+instantiation "fun" :: (type, leq) leq
+begin
 
-defs (overloaded)
+definition
   leq_fun_def: "f \<sqsubseteq> g \<equiv> \<forall>x. f x \<sqsubseteq> g x"
 
+instance ..
+
+end
+
 lemma leq_funI [intro?]: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
   by (unfold leq_fun_def) blast