equal
deleted
inserted
replaced
107 @{term "SQRT"}; (*Free ("SQRT", "'a")*) |
107 @{term "SQRT"}; (*Free ("SQRT", "'a")*) |
108 @{term "sqrt"}; (*Const ("NthRoot.sqrt", "RealDef.real => RealDef.real")*) |
108 @{term "sqrt"}; (*Const ("NthRoot.sqrt", "RealDef.real => RealDef.real")*) |
109 *} |
109 *} |
110 fun op_intern op_ = |
110 fun op_intern op_ = |
111 case assoc (ops, op_) of |
111 case assoc (ops, op_) of |
112 SOME op' => op' | NONE => raise error ("op_intern: no op= "^op_); |
112 SOME op' => op' | NONE => error ("op_intern: no op= "^op_); |
113 -----------------------*) |
113 -----------------------*) |
114 |
114 |
115 |
115 |
116 |
116 |
117 (* use"ME/solve.sml"; |
117 (* use"ME/solve.sml"; |