signature PGspec = sig type conv = Abbrev.conv val SET_SPEC_CONV : Thm.thm -> conv end;
HOL 4, Kananaskis-10