1structure ratPP = 2struct 3 4val _ = term_grammar.userSyntaxFns.register_userPP 5 {name = "rat.decimalfractions", 6 code = DecimalFractionPP.fraction{Thy = "rat", 7 Division = "rat_div", 8 fromNum = "rat_of_num"}} 9 10end 11
1structure ratPP = 2struct 3 4val _ = term_grammar.userSyntaxFns.register_userPP 5 {name = "rat.decimalfractions", 6 code = DecimalFractionPP.fraction{Thy = "rat", 7 Division = "rat_div", 8 fromNum = "rat_of_num"}} 9 10end 11