89 |
89 |
90 type squ = ptree; (* TODO: safe etc. *) |
90 type squ = ptree; (* TODO: safe etc. *) |
91 |
91 |
92 (*13.9.02-------------- |
92 (*13.9.02-------------- |
93 type ctr = (loc * pos) list; |
93 type ctr = (loc * pos) list; |
94 val ops = [("PLUS","Groups.plus_class.plus"),("MINUS","Groups.minus_class.minus"),("TIMES","op *"), |
94 val ops = [("PLUS","Groups.plus_class.plus"),("MINUS","Groups.minus_class.minus"),("TIMES","Groups.times_class.times"), |
95 ("cancel","cancel"),("pow","pow"),("sqrt","sqrt")]; |
95 ("cancel","cancel"),("pow","pow"),("sqrt","sqrt")]; |
96 ML {* |
96 ML {* |
97 @{term "PLUS"}; (*Free ("PLUS", "'a") : term*) |
97 @{term "PLUS"}; (*Free ("PLUS", "'a") : term*) |
98 @{term "plus"}; (*Const ("Groups.plus_class.plus", "'a => 'a => 'a")*) |
98 @{term "plus"}; (*Const ("Groups.plus_class.plus", "'a => 'a => 'a")*) |
99 @{term "MINUS"}; (*Free ("MINUS", "'a")*) |
99 @{term "MINUS"}; (*Free ("MINUS", "'a")*) |