signature CooperCore = sig include Abbrev val phase4_CONV : conv val phase5_CONV : conv end
HOL 4, Kananaskis-13