equal
deleted
inserted
replaced
986 lemma diff_strict_right_mono: "a < b \<Longrightarrow> a - c < b - c" |
986 lemma diff_strict_right_mono: "a < b \<Longrightarrow> a - c < b - c" |
987 by (simp add: field_simps) |
987 by (simp add: field_simps) |
988 |
988 |
989 end |
989 end |
990 |
990 |
991 ML_file "Tools/group_cancel.ML" |
991 ML_file \<open>Tools/group_cancel.ML\<close> |
992 |
992 |
993 simproc_setup group_cancel_add ("a + b::'a::ab_group_add") = |
993 simproc_setup group_cancel_add ("a + b::'a::ab_group_add") = |
994 \<open>fn phi => fn ss => try Group_Cancel.cancel_add_conv\<close> |
994 \<open>fn phi => fn ss => try Group_Cancel.cancel_add_conv\<close> |
995 |
995 |
996 simproc_setup group_cancel_diff ("a - b::'a::ab_group_add") = |
996 simproc_setup group_cancel_diff ("a - b::'a::ab_group_add") = |