--- a/doc-src/AxClass/Group/Group.thy Mon Dec 03 20:59:29 2001 +0100
+++ b/doc-src/AxClass/Group/Group.thy Mon Dec 03 20:59:57 2001 +0100
@@ -23,25 +23,25 @@
consts
times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<odot>" 70)
invers :: "'a \<Rightarrow> 'a" ("(_\<inv>)" [1000] 999)
- one :: 'a ("\<unit>")
+ one :: 'a ("\<one>")
text {*
\noindent Next we define class @{text monoid} of monoids with
- operations @{text \<odot>} and @{text \<unit>}. Note that multiple class
+ operations @{text \<odot>} and @{text \<one>}. Note that multiple class
axioms are allowed for user convenience --- they simply represent
the conjunction of their respective universal closures.
*}
axclass monoid \<subseteq> type
assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"
- left_unit: "\<unit> \<odot> x = x"
- right_unit: "x \<odot> \<unit> = x"
+ left_unit: "\<one> \<odot> x = x"
+ right_unit: "x \<odot> \<one> = x"
text {*
\noindent So class @{text monoid} contains exactly those types
- @{text \<tau>} where @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} and @{text "\<unit> \<Colon> \<tau>"}
+ @{text \<tau>} where @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} and @{text "\<one> \<Colon> \<tau>"}
are specified appropriately, such that @{text \<odot>} is associative and
- @{text \<unit>} is a left and right unit element for the @{text \<odot>}
+ @{text \<one>} is a left and right unit element for the @{text \<odot>}
operation.
*}
@@ -56,8 +56,8 @@
assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"
axclass group \<subseteq> semigroup
- left_unit: "\<unit> \<odot> x = x"
- left_inverse: "x\<inv> \<odot> x = \<unit>"
+ left_unit: "\<one> \<odot> x = x"
+ left_inverse: "x\<inv> \<odot> x = \<one>"
axclass agroup \<subseteq> group
commute: "x \<odot> y = y \<odot> x"
@@ -91,23 +91,23 @@
well-known laws of general groups.
*}
-theorem group_right_inverse: "x \<odot> x\<inv> = (\<unit>\<Colon>'a\<Colon>group)"
+theorem group_right_inverse: "x \<odot> x\<inv> = (\<one>\<Colon>'a\<Colon>group)"
proof -
- have "x \<odot> x\<inv> = \<unit> \<odot> (x \<odot> x\<inv>)"
+ have "x \<odot> x\<inv> = \<one> \<odot> (x \<odot> x\<inv>)"
by (simp only: group.left_unit)
- also have "... = \<unit> \<odot> x \<odot> x\<inv>"
+ also have "... = \<one> \<odot> x \<odot> x\<inv>"
by (simp only: semigroup.assoc)
also have "... = (x\<inv>)\<inv> \<odot> x\<inv> \<odot> x \<odot> x\<inv>"
by (simp only: group.left_inverse)
also have "... = (x\<inv>)\<inv> \<odot> (x\<inv> \<odot> x) \<odot> x\<inv>"
by (simp only: semigroup.assoc)
- also have "... = (x\<inv>)\<inv> \<odot> \<unit> \<odot> x\<inv>"
+ also have "... = (x\<inv>)\<inv> \<odot> \<one> \<odot> x\<inv>"
by (simp only: group.left_inverse)
- also have "... = (x\<inv>)\<inv> \<odot> (\<unit> \<odot> x\<inv>)"
+ also have "... = (x\<inv>)\<inv> \<odot> (\<one> \<odot> x\<inv>)"
by (simp only: semigroup.assoc)
also have "... = (x\<inv>)\<inv> \<odot> x\<inv>"
by (simp only: group.left_unit)
- also have "... = \<unit>"
+ also have "... = \<one>"
by (simp only: group.left_inverse)
finally show ?thesis .
qed
@@ -118,13 +118,13 @@
much easier.
*}
-theorem group_right_unit: "x \<odot> \<unit> = (x\<Colon>'a\<Colon>group)"
+theorem group_right_unit: "x \<odot> \<one> = (x\<Colon>'a\<Colon>group)"
proof -
- have "x \<odot> \<unit> = x \<odot> (x\<inv> \<odot> x)"
+ have "x \<odot> \<one> = x \<odot> (x\<inv> \<odot> x)"
by (simp only: group.left_inverse)
also have "... = x \<odot> x\<inv> \<odot> x"
by (simp only: semigroup.assoc)
- also have "... = \<unit> \<odot> x"
+ also have "... = \<one> \<odot> x"
by (simp only: group_right_inverse)
also have "... = x"
by (simp only: group.left_unit)
@@ -193,9 +193,9 @@
fix x y z :: "'a\<Colon>group"
show "x \<odot> y \<odot> z = x \<odot> (y \<odot> z)"
by (rule semigroup.assoc)
- show "\<unit> \<odot> x = x"
+ show "\<one> \<odot> x = x"
by (rule group.left_unit)
- show "x \<odot> \<unit> = x"
+ show "x \<odot> \<one> = x"
by (rule group_right_unit)
qed
@@ -227,13 +227,13 @@
\medskip As a typical example, we show that type @{typ bool} with
exclusive-or as @{text \<odot>} operation, identity as @{text \<inv>}, and
- @{term False} as @{text \<unit>} forms an Abelian group.
+ @{term False} as @{text \<one>} forms an Abelian group.
*}
defs (overloaded)
times_bool_def: "x \<odot> y \<equiv> x \<noteq> (y\<Colon>bool)"
inverse_bool_def: "x\<inv> \<equiv> x\<Colon>bool"
- unit_bool_def: "\<unit> \<equiv> False"
+ unit_bool_def: "\<one> \<equiv> False"
text {*
\medskip It is important to note that above $\DEFS$ are just
@@ -269,9 +269,9 @@
\medskip We could now also instantiate our group theory classes to
many other concrete types. For example, @{text "int \<Colon> agroup"}
(e.g.\ by defining @{text \<odot>} as addition, @{text \<inv>} as negation
- and @{text \<unit>} as zero) or @{text "list \<Colon> (type) semigroup"}
+ and @{text \<one>} as zero) or @{text "list \<Colon> (type) semigroup"}
(e.g.\ if @{text \<odot>} is defined as list append). Thus, the
- characteristic constants @{text \<odot>}, @{text \<inv>}, @{text \<unit>}
+ characteristic constants @{text \<odot>}, @{text \<inv>}, @{text \<one>}
really become overloaded, i.e.\ have different meanings on different
types.
*}
--- a/doc-src/AxClass/generated/Group.tex Mon Dec 03 20:59:29 2001 +0100
+++ b/doc-src/AxClass/generated/Group.tex Mon Dec 03 20:59:57 2001 +0100
@@ -30,25 +30,25 @@
\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
\ \ invers\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharparenleft}{\isacharunderscore}{\isasyminv}{\isacharparenright}{\isachardoublequote}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline
-\ \ one\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymunit}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
+\ \ one\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymone}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent Next we define class \isa{monoid} of monoids with
- operations \isa{{\isasymodot}} and \isa{{\isasymunit}}. Note that multiple class
+ operations \isa{{\isasymodot}} and \isa{{\isasymone}}. Note that multiple class
axioms are allowed for user convenience --- they simply represent
the conjunction of their respective universal closures.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{axclass}\ monoid\ {\isasymsubseteq}\ type\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}\isamarkupfalse%
+\ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}{\isasymone}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline
+\ \ right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequote}\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent So class \isa{monoid} contains exactly those types
- \isa{{\isasymtau}} where \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} and \isa{{\isasymunit}\ {\isasymColon}\ {\isasymtau}}
+ \isa{{\isasymtau}} where \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} and \isa{{\isasymone}\ {\isasymColon}\ {\isasymtau}}
are specified appropriately, such that \isa{{\isasymodot}} is associative and
- \isa{{\isasymunit}} is a left and right unit element for the \isa{{\isasymodot}}
+ \isa{{\isasymone}} is a left and right unit element for the \isa{{\isasymodot}}
operation.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -65,8 +65,8 @@
\isanewline
\isamarkupfalse%
\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
+\ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}{\isasymone}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline
+\ \ left{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequote}x{\isasyminv}\ {\isasymodot}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequote}\isanewline
\isanewline
\isamarkupfalse%
\isacommand{axclass}\ agroup\ {\isasymsubseteq}\ group\isanewline
@@ -98,16 +98,16 @@
well-known laws of general groups.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isacharparenleft}{\isasymunit}{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isacharparenleft}{\isasymone}{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline
\isamarkupfalse%
\isacommand{proof}\ {\isacharminus}\isanewline
\ \ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isasymunit}\ {\isasymodot}\ {\isacharparenleft}x\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{have}\ {\isachardoublequote}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isasymone}\ {\isasymodot}\ {\isacharparenleft}x\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequote}\isanewline
\ \ \ \ \isamarkupfalse%
\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline
\ \ \isamarkupfalse%
\isacommand{also}\ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymunit}\ {\isasymodot}\ x\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline
+\isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymone}\ {\isasymodot}\ x\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline
\ \ \ \ \isamarkupfalse%
\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline
\ \ \isamarkupfalse%
@@ -122,12 +122,12 @@
\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline
\ \ \isamarkupfalse%
\isacommand{also}\ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isasymunit}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline
+\isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isasymone}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline
\ \ \ \ \isamarkupfalse%
\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline
\ \ \isamarkupfalse%
\isacommand{also}\ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isacharparenleft}{\isasymunit}\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isacharparenleft}{\isasymone}\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequote}\isanewline
\ \ \ \ \isamarkupfalse%
\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline
\ \ \isamarkupfalse%
@@ -137,7 +137,7 @@
\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline
\ \ \isamarkupfalse%
\isacommand{also}\ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymunit}{\isachardoublequote}\isanewline
+\isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymone}{\isachardoublequote}\isanewline
\ \ \ \ \isamarkupfalse%
\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline
\ \ \isamarkupfalse%
@@ -152,11 +152,11 @@
much easier.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline
\isamarkupfalse%
\isacommand{proof}\ {\isacharminus}\isanewline
\ \ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}x{\isasyminv}\ {\isasymodot}\ x{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{have}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}x{\isasyminv}\ {\isasymodot}\ x{\isacharparenright}{\isachardoublequote}\isanewline
\ \ \ \ \isamarkupfalse%
\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline
\ \ \isamarkupfalse%
@@ -166,7 +166,7 @@
\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline
\ \ \isamarkupfalse%
\isacommand{also}\ \isamarkupfalse%
-\isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymunit}\ {\isasymodot}\ x{\isachardoublequote}\isanewline
+\isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymone}\ {\isasymodot}\ x{\isachardoublequote}\isanewline
\ \ \ \ \isamarkupfalse%
\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharparenright}\isanewline
\ \ \isamarkupfalse%
@@ -251,11 +251,11 @@
\ \ \ \ \isamarkupfalse%
\isacommand{by}\ {\isacharparenleft}rule\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline
\ \ \isamarkupfalse%
-\isacommand{show}\ {\isachardoublequote}{\isasymunit}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline
+\isacommand{show}\ {\isachardoublequote}{\isasymone}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline
\ \ \ \ \isamarkupfalse%
\isacommand{by}\ {\isacharparenleft}rule\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline
\ \ \isamarkupfalse%
-\isacommand{show}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ x{\isachardoublequote}\isanewline
+\isacommand{show}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequote}\isanewline
\ \ \ \ \isamarkupfalse%
\isacommand{by}\ {\isacharparenleft}rule\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharparenright}\isanewline
\isamarkupfalse%
@@ -289,13 +289,13 @@
\medskip As a typical example, we show that type \isa{bool} with
exclusive-or as \isa{{\isasymodot}} operation, identity as \isa{{\isasyminv}}, and
- \isa{False} as \isa{{\isasymunit}} forms an Abelian group.%
+ \isa{False} as \isa{{\isasymone}} forms an Abelian group.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
\ \ times{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymequiv}\ x\ {\isasymnoteq}\ {\isacharparenleft}y{\isasymColon}bool{\isacharparenright}{\isachardoublequote}\isanewline
\ \ inverse{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x{\isasyminv}\ {\isasymequiv}\ x{\isasymColon}bool{\isachardoublequote}\isanewline
-\ \ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}{\isasymunit}\ {\isasymequiv}\ False{\isachardoublequote}\isamarkupfalse%
+\ \ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}{\isasymone}\ {\isasymequiv}\ False{\isachardoublequote}\isamarkupfalse%
%
\begin{isamarkuptext}%
\medskip It is important to note that above $\DEFS$ are just
@@ -342,9 +342,9 @@
\medskip We could now also instantiate our group theory classes to
many other concrete types. For example, \isa{int\ {\isasymColon}\ agroup}
(e.g.\ by defining \isa{{\isasymodot}} as addition, \isa{{\isasyminv}} as negation
- and \isa{{\isasymunit}} as zero) or \isa{list\ {\isasymColon}\ {\isacharparenleft}type{\isacharparenright}\ semigroup}
+ and \isa{{\isasymone}} as zero) or \isa{list\ {\isasymColon}\ {\isacharparenleft}type{\isacharparenright}\ semigroup}
(e.g.\ if \isa{{\isasymodot}} is defined as list append). Thus, the
- characteristic constants \isa{{\isasymodot}}, \isa{{\isasyminv}}, \isa{{\isasymunit}}
+ characteristic constants \isa{{\isasymodot}}, \isa{{\isasyminv}}, \isa{{\isasymone}}
really become overloaded, i.e.\ have different meanings on different
types.%
\end{isamarkuptext}%
--- a/doc-src/AxClass/generated/isabellesym.sty Mon Dec 03 20:59:29 2001 +0100
+++ b/doc-src/AxClass/generated/isabellesym.sty Mon Dec 03 20:59:57 2001 +0100
@@ -7,6 +7,16 @@
% symbol definitions
+\newcommand{\isasymzero}{\isatext{\textzerooldstyle}} %requires textcomp
+\newcommand{\isasymone}{\isatext{\textoneoldstyle}} %requires textcomp
+\newcommand{\isasymtwo}{\isatext{\texttwooldstyle}} %requires textcomp
+\newcommand{\isasymthree}{\isatext{\textthreeoldstyle}} %requires textcomp
+\newcommand{\isasymfour}{\isatext{\textfouroldstyle}} %requires textcomp
+\newcommand{\isasymfive}{\isatext{\textfiveoldstyle}} %requires textcomp
+\newcommand{\isasymsix}{\isatext{\textsixoldstyle}} %requires textcomp
+\newcommand{\isasymseven}{\isatext{\textsevenoldstyle}} %requires textcomp
+\newcommand{\isasymeight}{\isatext{\texteightoldstyle}} %requires textcomp
+\newcommand{\isasymnine}{\isatext{\textnineoldstyle}} %requires textcomp
\newcommand{\isasymA}{\isamath{\mathcal{A}}}
\newcommand{\isasymB}{\isamath{\mathcal{B}}}
\newcommand{\isasymC}{\isamath{\mathcal{C}}}
@@ -307,7 +317,7 @@
\newcommand{\isasymnatural}{\isamath{\natural}}
\newcommand{\isasymsharp}{\isamath{\sharp}}
\newcommand{\isasymangle}{\isamath{\angle}}
-\newcommand{\isasymcopyright}{\isatext{\copyright}}
+\newcommand{\isasymcopyright}{\isatext{\rm\copyright}}
\newcommand{\isasymregistered}{\isatext{\rm\textregistered}}
\newcommand{\isasymhyphen}{\isatext{\rm-}}
\newcommand{\isasyminverse}{\isamath{{}^{-1}}}
@@ -319,20 +329,21 @@
\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}} %requires latin1
\newcommand{\isasymordfeminine}{\isatext{\rm\textordfeminine}}
\newcommand{\isasymordmasculine}{\isatext{\rm\textordmasculine}}
-\newcommand{\isasymsection}{\isatext{\S}}
-\newcommand{\isasymparagraph}{\isatext{\P}}
+\newcommand{\isasymsection}{\isatext{\rm\S}}
+\newcommand{\isasymparagraph}{\isatext{\rm\P}}
\newcommand{\isasymexclamdown}{\isatext{\rm\textexclamdown}}
\newcommand{\isasymquestiondown}{\isatext{\rm\textquestiondown}}
+\newcommand{\isasymeuro}{\isatext{\EUR}} %requires marvosym
\newcommand{\isasympounds}{\isamath{\pounds}}
\newcommand{\isasymyen}{\isatext{\yen}} %requires amssymb
\newcommand{\isasymcent}{\isatext{\cent}} %requires wasysym
\newcommand{\isasymcurrency}{\isatext{\currency}} %requires wasysym
\newcommand{\isasymdegree}{\isatext{\rm\textdegree}} %requires latin1
-\newcommand{\isasymwp}{\isamath{\wp}}
\newcommand{\isasymamalg}{\isamath{\amalg}}
\newcommand{\isasymmho}{\isamath{\mho}} %requires latexsym
\newcommand{\isasymlozenge}{\isamath{\lozenge}} %requires amssym
\newcommand{\isasymJoin}{\isamath{\Join}} %requires latexsym
+\newcommand{\isasymwp}{\isamath{\wp}}
\newcommand{\isasymwrong}{\isamath{\wr}}
\newcommand{\isasymspacespace}{\isamath{~~}}
\newcommand{\isasymacute}{\isatext{\'\relax}}