| changeset 15241 | a3949068537e |
| parent 15140 | 322485b816ac |
| child 19765 | dfe940911617 |
| 15240:e1e6db03beee | 15241:a3949068537e |
|---|---|
5 *) |
5 *) |
6 |
6 |
7 header{*Factorial Function*} |
7 header{*Factorial Function*} |
8 |
8 |
9 theory Fact |
9 theory Fact |
10 imports Real |
10 imports "../Real/Real" |
11 begin |
11 begin |
12 |
12 |
13 consts fact :: "nat => nat" |
13 consts fact :: "nat => nat" |
14 primrec |
14 primrec |
15 fact_0: "fact 0 = 1" |
15 fact_0: "fact 0 = 1" |