equal
deleted
inserted
replaced
47 (see 'fun thy_containing_thm', 'fun thy_containing_rls' etc.) |
47 (see 'fun thy_containing_thm', 'fun thy_containing_rls' etc.) |
48 TODO: introduce to pbl, met.*) |
48 TODO: introduce to pbl, met.*) |
49 type guh = string; |
49 type guh = string; |
50 val e_guh = "e_guh":guh; |
50 val e_guh = "e_guh":guh; |
51 |
51 |
52 type xml = string; |
52 type xml = string; (* rm together with old code replaced by XML.tree *) |
|
53 fun string_to_bool "true" = true |
|
54 | string_to_bool "false" = false |
|
55 | string_to_bool str = error ("string_to_bool: arg = " ^ str) |
53 |
56 |
54 (* eval function calling sml code during rewriting. |
57 (* eval function calling sml code during rewriting. |
55 Unifying "type cal" and "type calc" would make Lucas-Interpretation more efficient, |
58 Unifying "type cal" and "type calc" would make Lucas-Interpretation more efficient, |
56 see "fun rule2stac": instead of |
59 see "fun rule2stac": instead of |
57 Calc: calID * eval_fn -> rule |
60 Calc: calID * eval_fn -> rule |