# HG changeset patch # User haftmann # Date 1265700492 -3600 # Node ID be1e25a62ec8e4a79a3b9792d9a72ab636aba64b # Parent 6088dfd5f9c8cfa91b8a8cd45edb8c9f1e56d7e5 adjusted to cs. 9f841f20dca6 diff -r 6088dfd5f9c8 -r be1e25a62ec8 doc-src/Main/Docs/Main_Doc.thy --- a/doc-src/Main/Docs/Main_Doc.thy Mon Feb 08 15:54:01 2010 -0800 +++ b/doc-src/Main/Docs/Main_Doc.thy Tue Feb 09 08:28:12 2010 +0100 @@ -297,7 +297,7 @@ \section{Algebra} -Theories @{theory OrderedGroup}, @{theory Ring_and_Field} and @{theory +Theories @{theory Groups}, @{theory Rings}, @{theory Fields} and @{theory Divides} define a large collection of classes describing common algebraic structures from semigroups up to fields. Everything is done in terms of overloaded operators: diff -r 6088dfd5f9c8 -r be1e25a62ec8 doc-src/Main/Docs/document/Main_Doc.tex --- a/doc-src/Main/Docs/document/Main_Doc.tex Mon Feb 08 15:54:01 2010 -0800 +++ b/doc-src/Main/Docs/document/Main_Doc.tex Tue Feb 09 08:28:12 2010 +0100 @@ -308,7 +308,7 @@ \section{Algebra} -Theories \isa{OrderedGroup}, \isa{Ring{\isacharunderscore}and{\isacharunderscore}Field} and \isa{Divides} define a large collection of classes describing common algebraic +Theories \isa{Groups}, \isa{Rings}, \isa{Fields} and \isa{Divides} define a large collection of classes describing common algebraic structures from semigroups up to fields. Everything is done in terms of overloaded operators: