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 Open_locale "sylow"; |
14 Open_locale "sylow"; |
10 |
15 |
11 val prime_p = thm "prime_p"; |
16 val prime_p = thm "prime_p"; |