equal
deleted
inserted
replaced
4 Normalization by evaluation, based on generic code generator. |
4 Normalization by evaluation, based on generic code generator. |
5 *) |
5 *) |
6 |
6 |
7 signature NBE = |
7 signature NBE = |
8 sig |
8 sig |
9 val dynamic_eval_conv: cterm -> thm |
9 val dynamic_eval_conv: conv |
10 val dynamic_eval_value: theory -> term -> term |
10 val dynamic_eval_value: theory -> term -> term |
11 |
11 |
12 datatype Univ = |
12 datatype Univ = |
13 Const of int * Univ list (*named (uninterpreted) constants*) |
13 Const of int * Univ list (*named (uninterpreted) constants*) |
14 | DFree of string * int (*free (uninterpreted) dictionary parameters*) |
14 | DFree of string * int (*free (uninterpreted) dictionary parameters*) |