innermost_params;

(simp add: point.make_def);

provodes induct/cases for use with corresponding Isar methods; "record" operation (acts as type cast); internal field_inducts, field_cases; make_defs no longer declared as simps; fixed printing of fixed records;

further 1.73 changes: added fix_direct, simplified assume interface;