equal
deleted
inserted
replaced
89 |
89 |
90 val denom1 = parseNEW ctxt "(z + -1 * (1 / 2))::real" |> the; |
90 val denom1 = parseNEW ctxt "(z + -1 * (1 / 2))::real" |> the; |
91 val denom2 = parseNEW ctxt "(z + -1 * (-1 / 4))::real" |> the; |
91 val denom2 = parseNEW ctxt "(z + -1 * (-1 / 4))::real" |> the; |
92 |
92 |
93 val test = HOLogic.mk_binop "Groups.plus_class.plus" |
93 val test = HOLogic.mk_binop "Groups.plus_class.plus" |
94 (HOLogic.mk_binop "Fields.inverse_class.divide" (A_var, denom1), |
94 (HOLogic.mk_binop "Rings.divide_class.divide" (A_var, denom1), |
95 HOLogic.mk_binop "Fields.inverse_class.divide" (B_var, denom2)); |
95 HOLogic.mk_binop "Rings.divide_class.divide" (B_var, denom2)); |
96 |
96 |
97 if term2str test = "?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))" then () |
97 if term2str test = "?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))" then () |
98 else error "HOLogic.mk_binop broken ?"; |
98 else error "HOLogic.mk_binop broken ?"; |
99 |
99 |
100 (* Logic.unvarify_global test |
100 (* Logic.unvarify_global test |