--- 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
--- 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)
--- 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 {*
--- 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"
--- 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
--- 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
--- 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}%
--- 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
--- 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" ..
--- 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" ..
--- 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"
--- 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"