equal
deleted
inserted
replaced
70 val (lpath, rpath) = find_common coeff_ord (atoms lhs) (atoms rhs) |
70 val (lpath, rpath) = find_common coeff_ord (atoms lhs) (atoms rhs) |
71 val lconv = move_to_front lpath |
71 val lconv = move_to_front lpath |
72 val rconv = move_to_front rpath |
72 val rconv = move_to_front rpath |
73 val conv1 = Conv.combination_conv (Conv.arg_conv lconv) rconv |
73 val conv1 = Conv.combination_conv (Conv.arg_conv lconv) rconv |
74 val conv = conv1 then_conv Conv.rewr_conv rule |
74 val conv = conv1 then_conv Conv.rewr_conv rule |
75 in conv ct handle Cancel => raise CTERM ("no_conversion", []) end |
75 in conv ct end |
|
76 handle Cancel => raise CTERM ("no_conversion", []) |
76 |
77 |
77 val cancel_diff_conv = cancel_conv (mk_meta_eq @{thm add_diff_cancel_left}) |
78 val cancel_diff_conv = cancel_conv (mk_meta_eq @{thm add_diff_cancel_left}) |
78 val cancel_eq_conv = cancel_conv (mk_meta_eq @{thm add_left_cancel}) |
79 val cancel_eq_conv = cancel_conv (mk_meta_eq @{thm add_left_cancel}) |
79 val cancel_le_conv = cancel_conv (mk_meta_eq @{thm add_le_cancel_left}) |
80 val cancel_le_conv = cancel_conv (mk_meta_eq @{thm add_le_cancel_left}) |
80 val cancel_less_conv = cancel_conv (mk_meta_eq @{thm add_less_cancel_left}) |
81 val cancel_less_conv = cancel_conv (mk_meta_eq @{thm add_less_cancel_left}) |