- Equivariance simpset used in proofs of strong induction and inversion rules now contains perm_simproc_app and perm_simproc_fun as well - first_order_matchs now eta-contracts terms before matching - Rewrote code for proving strong inversion rule to avoid failure when one of the arguments of the inductive predicate has an atom type

pprint: back to proper output of markup, with workaround for Poly/ML crash;

back to 1.36 (Poly/ML crash!?);