| author | paulson |
| Tue, 18 Mar 2003 18:07:06 +0100 | |
| changeset 13870 | cf947d1ec5ff |
| parent 13745 | a31e04831dd1 |
| child 13906 | eefdd6b14508 |
| permissions | -rw-r--r-- |
|
13583
5fcc8bf538ee
converted to Isar and using new "implicit structures" instead of Sigma, etc
paulson
parents:
11443
diff
changeset
|
1 |
no_document use_thy "FuncSet"; |
|
11370
680946254afe
new GroupTheory example, e.g. the Sylow theorem (preliminary version)
paulson
parents:
diff
changeset
|
2 |
|
|
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
13745
diff
changeset
|
3 |
use_thy "Bij"; |
|
13745
a31e04831dd1
HOL/GroupTheory/Summation.thy added: summation operator for abelian groups.
ballarin
parents:
13590
diff
changeset
|
4 |
use_thy "Summation"; |