src/HOL/GroupTheory/ROOT.ML
author paulson
Sun, 10 Jun 2001 08:03:35 +0200
changeset 11370 680946254afe
child 11394 e88c2c89f98e
permissions -rw-r--r--
new GroupTheory example, e.g. the Sylow theorem (preliminary version)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11370
680946254afe new GroupTheory example, e.g. the Sylow theorem (preliminary version)
paulson
parents:
diff changeset
     1
680946254afe new GroupTheory example, e.g. the Sylow theorem (preliminary version)
paulson
parents:
diff changeset
     2
no_document use_thy "Primes";
680946254afe new GroupTheory example, e.g. the Sylow theorem (preliminary version)
paulson
parents:
diff changeset
     3
680946254afe new GroupTheory example, e.g. the Sylow theorem (preliminary version)
paulson
parents:
diff changeset
     4
use_thy "Sylow";