add testing framework for generated code

correct code equation for term_of on integer

merged

add code equation for term_of on integer

added lemmas contributed by Rene Thiemann

attach modifier only later, to avoid interference as e.g. in "simp add: foo [simplified] bar";

tuned whitespace;

clarified ML toplevel pp: avoid ML output to be attached to inlined binding positions;

merged

made SML/NJ happy;