| author | paulson |
| Wed, 09 Apr 2003 12:51:49 +0200 | |
| changeset 13906 | eefdd6b14508 |
| parent 13870 | cf947d1ec5ff |
| child 13943 | 83d842ccd4aa |
| 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"; |