equal
deleted
inserted
replaced
5 moved elsewhere or otherwise cleaned up. |
5 moved elsewhere or otherwise cleaned up. |
6 *) |
6 *) |
7 |
7 |
8 signature FUNCTION_LIB = |
8 signature FUNCTION_LIB = |
9 sig |
9 sig |
10 val function_defs: bool Config.T |
10 val function_internals: bool Config.T |
11 |
11 |
12 val plural: string -> string -> 'a list -> string |
12 val plural: string -> string -> 'a list -> string |
13 |
13 |
14 val dest_all_all: term -> term list * term |
14 val dest_all_all: term -> term list * term |
15 |
15 |
30 end |
30 end |
31 |
31 |
32 structure Function_Lib: FUNCTION_LIB = |
32 structure Function_Lib: FUNCTION_LIB = |
33 struct |
33 struct |
34 |
34 |
35 val function_defs = Attrib.setup_config_bool @{binding function_defs} (K false) |
35 val function_internals = Attrib.setup_config_bool @{binding function_internals} (K false) |
36 |
36 |
37 |
37 |
38 (* "The variable" ^ plural " is" "s are" vs *) |
38 (* "The variable" ^ plural " is" "s are" vs *) |
39 fun plural sg pl [x] = sg |
39 fun plural sg pl [x] = sg |
40 | plural sg pl _ = pl |
40 | plural sg pl _ = pl |