signature ratReduce = sig include Abbrev val RAT_ADD_CONV : conv val RAT_MUL_CONV : conv end
HOL 4, Trindemossen-1