equal
deleted
inserted
replaced
3 Copyright : 1998 University of Cambridge |
3 Copyright : 1998 University of Cambridge |
4 Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
4 Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
5 The integer version of factorial and other additions by Jeremy Avigad. |
5 The integer version of factorial and other additions by Jeremy Avigad. |
6 *) |
6 *) |
7 |
7 |
8 header{*Factorial Function*} |
8 section{*Factorial Function*} |
9 |
9 |
10 theory Fact |
10 theory Fact |
11 imports Main |
11 imports Main |
12 begin |
12 begin |
13 |
13 |