Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/GroupTheory/ROOT.ML
author wenzelm
Sat, 13 Oct 2001 20:32:07 +0200
changeset 11741 470e608d7a74
parent 11443 77ed7e2b56c8
child 13583 5fcc8bf538ee
permissions -rw-r--r--
generic theorem kinds ("theorem", "lemma" etc.);
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









11394






e88c2c89f98e
Locale-based group theory proofs



paulson


parents: 
11370

diff
changeset




     4


use_thy "DirProd";








11370






680946254afe
new GroupTheory example, e.g. the Sylow theorem (preliminary version)



paulson


parents: 

diff
changeset




     5


use_thy "Sylow";








11443






77ed7e2b56c8
The final version of Florian Kammueller's proofs



paulson


parents: 
11394

diff
changeset




     6


use_thy "RingConstr";













77ed7e2b56c8
The final version of Florian Kammueller's proofs



paulson


parents: 
11394

diff
changeset




     7


use_thy "PiSets";















isabelle