:: deftheorem defines Gauss_RAT_Ring GAUSSINT:def 17 :
Gauss_RAT_Ring = doubleLoopStr(# G_RAT_SET,g_rat_add,g_rat_mult,(In (1,G_RAT_SET)),(In (0,G_RAT_SET)) #);