# HG changeset patch
# User wenzelm
# Date 982006992 -3600
# Node ID b301d1f725524f1d53faa3d0269f214acbf9f3dc
# Parent  a3299b153741fae409376076f6f7250eba49390f
\<subseteq>;

diff -r a3299b153741 -r b301d1f72552 doc-src/AxClass/Group/Group.thy
--- a/doc-src/AxClass/Group/Group.thy	Sun Feb 11 20:38:40 2001 +0100
+++ b/doc-src/AxClass/Group/Group.thy	Mon Feb 12 20:43:12 2001 +0100
@@ -32,7 +32,7 @@
  conjunction of their respective universal closures.
 *}
 
-axclass monoid < "term"
+axclass monoid \<subseteq> "term"
   assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"
   left_unit: "\<unit> \<odot> x = x"
   right_unit: "x \<odot> \<unit> = x"
@@ -52,14 +52,14 @@
  class name, so we may re-use common names such as @{text assoc}.
 *}
 
-axclass semigroup < "term"
+axclass semigroup \<subseteq> "term"
   assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"
 
-axclass group < semigroup
+axclass group \<subseteq> semigroup
   left_unit: "\<unit> \<odot> x = x"
   left_inverse: "x\<inv> \<odot> x = \<unit>"
 
-axclass agroup < group
+axclass agroup \<subseteq> group
   commute: "x \<odot> y = y \<odot> x"
 
 text {*
@@ -181,14 +181,14 @@
  \end{figure}
 *}
 
-instance monoid < semigroup
+instance monoid \<subseteq> semigroup
 proof
   fix x y z :: "'a\<Colon>monoid"
   show "x \<odot> y \<odot> z = x \<odot> (y \<odot> z)"
     by (rule monoid.assoc)
 qed
 
-instance group < monoid
+instance group \<subseteq> monoid
 proof
   fix x y z :: "'a\<Colon>group"
   show "x \<odot> y \<odot> z = x \<odot> (y \<odot> z)"
@@ -216,7 +216,7 @@
 
 text {*
  So far we have covered the case of the form $\INSTANCE$~@{text
- "c\<^sub>1 < c\<^sub>2"}, namely \emph{abstract instantiation} ---
+ "c\<^sub>1 \<subseteq> c\<^sub>2"}, namely \emph{abstract instantiation} ---
  $c@1$ is more special than @{text "c\<^sub>1"} and thus an instance
  of @{text "c\<^sub>2"}.  Even more interesting for practical
  applications are \emph{concrete instantiations} of axiomatic type
diff -r a3299b153741 -r b301d1f72552 doc-src/AxClass/Group/Product.thy
--- a/doc-src/AxClass/Group/Product.thy	Sun Feb 11 20:38:40 2001 +0100
+++ b/doc-src/AxClass/Group/Product.thy	Mon Feb 12 20:43:12 2001 +0100
@@ -18,7 +18,7 @@
 *}
 
 axclass
-  product < "term"
+  product \<subseteq> "term"
 consts
   product :: "'a\<Colon>product \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<odot>" 70)
 
diff -r a3299b153741 -r b301d1f72552 doc-src/AxClass/Group/Semigroups.thy
--- a/doc-src/AxClass/Group/Semigroups.thy	Sun Feb 11 20:38:40 2001 +0100
+++ b/doc-src/AxClass/Group/Semigroups.thy	Mon Feb 12 20:43:12 2001 +0100
@@ -18,7 +18,7 @@
 
 consts
   times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<odot>" 70)
-axclass semigroup < "term"
+axclass semigroup \<subseteq> "term"
   assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"
 
 text {*
@@ -41,7 +41,7 @@
 
 consts
   plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<oplus>" 70)
-axclass plus_semigroup < "term"
+axclass plus_semigroup \<subseteq> "term"
   assoc: "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
 
 text {*
diff -r a3299b153741 -r b301d1f72552 doc-src/AxClass/Nat/NatClass.thy
--- a/doc-src/AxClass/Nat/NatClass.thy	Sun Feb 11 20:38:40 2001 +0100
+++ b/doc-src/AxClass/Nat/NatClass.thy	Mon Feb 12 20:43:12 2001 +0100
@@ -19,7 +19,7 @@
   Suc :: "'a \<Rightarrow> 'a"
   rec :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
 
-axclass nat < "term"
+axclass nat \<subseteq> "term"
   induct: "P(\<zero>) \<Longrightarrow> (\<And>x. P(x) \<Longrightarrow> P(Suc(x))) \<Longrightarrow> P(n)"
   Suc_inject: "Suc(m) = Suc(n) \<Longrightarrow> m = n"
   Suc_neq_0: "Suc(m) = \<zero> \<Longrightarrow> R"
diff -r a3299b153741 -r b301d1f72552 doc-src/AxClass/generated/Group.tex
--- a/doc-src/AxClass/generated/Group.tex	Sun Feb 11 20:38:40 2001 +0100
+++ b/doc-src/AxClass/generated/Group.tex	Mon Feb 12 20:43:12 2001 +0100
@@ -32,7 +32,7 @@
  axioms are allowed for user convenience --- they simply represent the
  conjunction of their respective universal closures.%
 \end{isamarkuptext}%
-\isacommand{axclass}\ monoid\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
+\isacommand{axclass}\ monoid\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
 \ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline
 \ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}{\isasymunit}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline
 \ \ right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ x{\isachardoublequote}%
@@ -49,14 +49,14 @@
  that the names of class axioms are automatically qualified with each
  class name, so we may re-use common names such as \isa{assoc}.%
 \end{isamarkuptext}%
-\isacommand{axclass}\ semigroup\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
+\isacommand{axclass}\ semigroup\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
 \ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline
 \isanewline
-\isacommand{axclass}\ group\ {\isacharless}\ semigroup\isanewline
+\isacommand{axclass}\ group\ {\isasymsubseteq}\ semigroup\isanewline
 \ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}{\isasymunit}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline
 \ \ left{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequote}x{\isasyminv}\ {\isasymodot}\ x\ {\isacharequal}\ {\isasymunit}{\isachardoublequote}\isanewline
 \isanewline
-\isacommand{axclass}\ agroup\ {\isacharless}\ group\isanewline
+\isacommand{axclass}\ agroup\ {\isasymsubseteq}\ group\isanewline
 \ \ commute{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isacharequal}\ y\ {\isasymodot}\ x{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent Class \isa{group} inherits associativity of \isa{{\isasymodot}}
@@ -165,14 +165,14 @@
    \end{center}
  \end{figure}%
 \end{isamarkuptext}%
-\isacommand{instance}\ monoid\ {\isacharless}\ semigroup\isanewline
+\isacommand{instance}\ monoid\ {\isasymsubseteq}\ semigroup\isanewline
 \isacommand{proof}\isanewline
 \ \ \isacommand{fix}\ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}monoid{\isachardoublequote}\isanewline
 \ \ \isacommand{show}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline
 \ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ monoid{\isachardot}assoc{\isacharparenright}\isanewline
 \isacommand{qed}\isanewline
 \isanewline
-\isacommand{instance}\ group\ {\isacharless}\ monoid\isanewline
+\isacommand{instance}\ group\ {\isasymsubseteq}\ monoid\isanewline
 \isacommand{proof}\isanewline
 \ \ \isacommand{fix}\ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}group{\isachardoublequote}\isanewline
 \ \ \isacommand{show}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline
@@ -198,7 +198,7 @@
 }
 %
 \begin{isamarkuptext}%
-So far we have covered the case of the form $\INSTANCE$~\isa{c\isactrlsub {\isadigit{1}}\ {\isacharless}\ c\isactrlsub {\isadigit{2}}}, namely \emph{abstract instantiation} ---
+So far we have covered the case of the form $\INSTANCE$~\isa{c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}}, namely \emph{abstract instantiation} ---
  $c@1$ is more special than \isa{c\isactrlsub {\isadigit{1}}} and thus an instance
  of \isa{c\isactrlsub {\isadigit{2}}}.  Even more interesting for practical
  applications are \emph{concrete instantiations} of axiomatic type
diff -r a3299b153741 -r b301d1f72552 doc-src/AxClass/generated/NatClass.tex
--- a/doc-src/AxClass/generated/NatClass.tex	Sun Feb 11 20:38:40 2001 +0100
+++ b/doc-src/AxClass/generated/NatClass.tex	Mon Feb 12 20:43:12 2001 +0100
@@ -20,7 +20,7 @@
 \ \ Suc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline
 \ \ rec\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline
 \isanewline
-\isacommand{axclass}\ nat\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
+\isacommand{axclass}\ nat\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
 \ \ induct{\isacharcolon}\ {\isachardoublequote}P{\isacharparenleft}{\isasymzero}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ P{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ P{\isacharparenleft}Suc{\isacharparenleft}x{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ P{\isacharparenleft}n{\isacharparenright}{\isachardoublequote}\isanewline
 \ \ Suc{\isacharunderscore}inject{\isacharcolon}\ {\isachardoublequote}Suc{\isacharparenleft}m{\isacharparenright}\ {\isacharequal}\ Suc{\isacharparenleft}n{\isacharparenright}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isanewline
 \ \ Suc{\isacharunderscore}neq{\isacharunderscore}{\isadigit{0}}{\isacharcolon}\ {\isachardoublequote}Suc{\isacharparenleft}m{\isacharparenright}\ {\isacharequal}\ {\isasymzero}\ {\isasymLongrightarrow}\ R{\isachardoublequote}\isanewline
diff -r a3299b153741 -r b301d1f72552 doc-src/AxClass/generated/Product.tex
--- a/doc-src/AxClass/generated/Product.tex	Sun Feb 11 20:38:40 2001 +0100
+++ b/doc-src/AxClass/generated/Product.tex	Mon Feb 12 20:43:12 2001 +0100
@@ -18,7 +18,7 @@
  syntactic type classes.%
 \end{isamarkuptext}%
 \isacommand{axclass}\isanewline
-\ \ product\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
+\ \ product\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
 \isacommand{consts}\isanewline
 \ \ product\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymodot}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}%
 \begin{isamarkuptext}%
diff -r a3299b153741 -r b301d1f72552 doc-src/AxClass/generated/Semigroups.tex
--- a/doc-src/AxClass/generated/Semigroups.tex	Sun Feb 11 20:38:40 2001 +0100
+++ b/doc-src/AxClass/generated/Semigroups.tex	Mon Feb 12 20:43:12 2001 +0100
@@ -19,7 +19,7 @@
 \end{isamarkuptext}%
 \isacommand{consts}\isanewline
 \ \ times\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymodot}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
-\isacommand{axclass}\ semigroup\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
+\isacommand{axclass}\ semigroup\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
 \ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent Above we have first declared a polymorphic constant \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} and then defined the class \isa{semigroup} of
@@ -38,7 +38,7 @@
 \end{isamarkuptext}%
 \isacommand{consts}\isanewline
 \ \ plus\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
-\isacommand{axclass}\ plus{\isacharunderscore}semigroup\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
+\isacommand{axclass}\ plus{\isacharunderscore}semigroup\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
 \ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymoplus}\ y{\isacharparenright}\ {\isasymoplus}\ z\ {\isacharequal}\ x\ {\isasymoplus}\ {\isacharparenleft}y\ {\isasymoplus}\ z{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent Even if classes \isa{plus{\isacharunderscore}semigroup} and \isa{semigroup} both represent semigroups in a sense, they are certainly
diff -r a3299b153741 -r b301d1f72552 src/HOL/Lattice/CompleteLattice.thy
--- a/src/HOL/Lattice/CompleteLattice.thy	Sun Feb 11 20:38:40 2001 +0100
+++ b/src/HOL/Lattice/CompleteLattice.thy	Mon Feb 12 20:43:12 2001 +0100
@@ -16,7 +16,7 @@
   bounds (see \S\ref{sec:connect-bounds}).
 *}
 
-axclass complete_lattice < partial_order
+axclass complete_lattice \<subseteq> partial_order
   ex_Inf: "\<exists>inf. is_Inf A inf"
 
 theorem ex_Sup: "\<exists>sup::'a::complete_lattice. is_Sup A sup"
@@ -274,7 +274,7 @@
   thus ?thesis by (simp only: is_Sup_binary)
 qed
 
-instance complete_lattice < lattice
+instance complete_lattice \<subseteq> lattice
 proof
   fix x y :: "'a::complete_lattice"
   from is_inf_binary show "\<exists>inf. is_inf x y inf" ..
diff -r a3299b153741 -r b301d1f72552 src/HOL/Lattice/Lattice.thy
--- a/src/HOL/Lattice/Lattice.thy	Sun Feb 11 20:38:40 2001 +0100
+++ b/src/HOL/Lattice/Lattice.thy	Mon Feb 12 20:43:12 2001 +0100
@@ -15,7 +15,7 @@
   as well).
 *}
 
-axclass lattice < partial_order
+axclass lattice \<subseteq> partial_order
   ex_inf: "\<exists>inf. is_inf x y inf"
   ex_sup: "\<exists>sup. is_sup x y sup"
 
@@ -360,7 +360,7 @@
   with leq_linear show "?max \<sqsubseteq> z" by (auto simp add: maximum_def)
 qed
 
-instance linear_order < lattice
+instance linear_order \<subseteq> lattice
 proof
   fix x y :: "'a::linear_order"
   from is_inf_minimum show "\<exists>inf. is_inf x y inf" ..
diff -r a3299b153741 -r b301d1f72552 src/HOL/Library/Quotient.thy
--- a/src/HOL/Library/Quotient.thy	Sun Feb 11 20:38:40 2001 +0100
+++ b/src/HOL/Library/Quotient.thy	Mon Feb 12 20:43:12 2001 +0100
@@ -23,11 +23,11 @@
  "\<sim> :: 'a => 'a => bool"}.
 *}
 
-axclass eqv < "term"
+axclass eqv \<subseteq> "term"
 consts
   eqv :: "('a::eqv) => 'a => bool"    (infixl "\<sim>" 50)
 
-axclass equiv < eqv
+axclass equiv \<subseteq> eqv
   equiv_refl [intro]: "x \<sim> x"
   equiv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
   equiv_sym [elim?]: "x \<sim> y ==> y \<sim> x"
diff -r a3299b153741 -r b301d1f72552 src/HOL/Library/Ring_and_Field.thy
--- a/src/HOL/Library/Ring_and_Field.thy	Sun Feb 11 20:38:40 2001 +0100
+++ b/src/HOL/Library/Ring_and_Field.thy	Mon Feb 12 20:43:12 2001 +0100
@@ -12,7 +12,7 @@
 
 subsection {* Abstract algebraic structures *}
 
-axclass ring < zero, plus, minus, times, number
+axclass ring \<subseteq> zero, plus, minus, times, number
   add_assoc: "(a + b) + c = a + (b + c)"
   add_commute: "a + b = b + a"
   left_zero [simp]: "0 + a = a"
@@ -26,18 +26,18 @@
 
   left_distrib: "(a + b) * c = a * c + b * c"
 
-axclass ordered_ring < ring, linorder
+axclass ordered_ring \<subseteq> ring, linorder
   add_left_mono: "a \<le> b ==> c + a \<le> c + b"
   mult_strict_left_mono: "a < b ==> 0 < c ==> c * a < c * b"
   abs_if: "\<bar>a\<bar> = (if a < 0 then -a else a)"
 
-axclass field < ring, inverse
+axclass field \<subseteq> ring, inverse
   left_inverse [simp]: "a \<noteq> 0 ==> inverse a * a = #1"
   divide_inverse: "b \<noteq> 0 ==> a / b = a * inverse b"
 
-axclass ordered_field < ordered_ring, field
+axclass ordered_field \<subseteq> ordered_ring, field
 
-axclass division_by_zero < zero, inverse
+axclass division_by_zero \<subseteq> zero, inverse
   inverse_zero: "inverse 0 = 0"
   divide_zero: "a / 0 = 0"