equal
deleted
inserted
replaced
1 (* Title: HOL/ex/Lagrange.thy |
1 (* Title: HOL/ex/Lagrange.thy |
2 Author: Tobias Nipkow |
2 Author: Tobias Nipkow |
3 Copyright 1996 TU Muenchen |
3 Copyright 1996 TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 header {* A lemma for Lagrange's theorem *} |
6 section {* A lemma for Lagrange's theorem *} |
7 |
7 |
8 theory Lagrange imports Main begin |
8 theory Lagrange imports Main begin |
9 |
9 |
10 text {* This theory only contains a single theorem, which is a lemma |
10 text {* This theory only contains a single theorem, which is a lemma |
11 in Lagrange's proof that every natural number is the sum of 4 squares. |
11 in Lagrange's proof that every natural number is the sum of 4 squares. |