equal
deleted
inserted
replaced
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Stefan Berghofer and Norbert Voelker |
3 Author: Stefan Berghofer and Norbert Voelker |
4 Copyright 1998 TU Muenchen |
4 Copyright 1998 TU Muenchen |
5 |
5 |
6 Package for defining functions on datatypes by primitive recursion. |
6 Package for defining functions on datatypes by primitive recursion. |
7 |
|
8 TODO: |
|
9 - add_primrec(_i): improve prep of args; |
|
10 - quiet_mode (!?); |
|
11 *) |
7 *) |
12 |
8 |
13 signature PRIMREC_PACKAGE = |
9 signature PRIMREC_PACKAGE = |
14 sig |
10 sig |
15 val add_primrec: string -> ((string * string) * Args.src list) list |
11 val add_primrec: string -> ((bstring * string) * Args.src list) list |
16 -> theory -> theory * thm list |
12 -> theory -> theory * thm list |
17 val add_primrec_i: string -> ((string * term) * theory attribute list) list |
13 val add_primrec_i: string -> ((bstring * term) * theory attribute list) list |
18 -> theory -> theory * thm list |
14 -> theory -> theory * thm list |
19 end; |
15 end; |
20 |
16 |
21 structure PrimrecPackage : PRIMREC_PACKAGE = |
17 structure PrimrecPackage : PRIMREC_PACKAGE = |
22 struct |
18 struct |