equal
deleted
inserted
replaced
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Florian Kammueller, with new proofs by L C Paulson |
3 Author: Florian Kammueller, with new proofs by L C Paulson |
4 Copyright 1998-2001 University of Cambridge |
4 Copyright 1998-2001 University of Cambridge |
5 |
5 |
6 Sylow's theorem using locales (combinatorial argument in Exponent.thy) |
6 Sylow's theorem using locales (combinatorial argument in Exponent.thy) |
|
7 |
|
8 See Florian Kamm\"uller and L. C. Paulson, |
|
9 A Formal Proof of Sylow's theorem: |
|
10 An Experiment in Abstract Algebra with Isabelle HOL |
|
11 J. Automated Reasoning 23 (1999), 235-264 |
7 *) |
12 *) |
8 |
13 |
9 Sylow = Coset + |
14 Sylow = Coset + |
10 |
15 |
11 locale sylow = coset + |
16 locale sylow = coset + |