# HG changeset patch
# User haftmann
# Date 1279563829 -7200
# Node ID 0d8058e0c270dcbd8266c0ab8e0685f3482d027f
# Parent  d78a3cdbd615acad9ec200e9ec7b034ebe1486d3
keep explicit diff_def as legacy theorem; modernized abel_cancel simproc setup

diff -r d78a3cdbd615 -r 0d8058e0c270 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Mon Jul 19 20:19:03 2010 +0200
+++ b/src/HOL/Groups.thy	Mon Jul 19 20:23:49 2010 +0200
@@ -796,21 +796,21 @@
   "a - b = c - d \<Longrightarrow> a < b \<longleftrightarrow> c < d"
   by (auto simp only: less_iff_diff_less_0 [of a b] less_iff_diff_less_0 [of c d])
 
-lemma diff_eq_diff_less_eq': -- "FIXME orientation"
-  "a - b = c - d \<Longrightarrow> b \<le> a \<longleftrightarrow> d \<le> c"
-proof -
-  assume "a - b = c - d"
-  then have "b - a = d - c" by (simp add: algebra_simps)
-  then show "b \<le> a \<longleftrightarrow> d \<le> c" by (auto simp only: le_iff_diff_le_0 [of b a] le_iff_diff_le_0 [of d c])
-qed
+lemma diff_eq_diff_less_eq:
+  "a - b = c - d \<Longrightarrow> a \<le> b \<longleftrightarrow> c \<le> d"
+  by (auto simp only: le_iff_diff_le_0 [of a b] le_iff_diff_le_0 [of c d])
 
 end
 
 use "~~/src/HOL/Tools/abel_cancel.ML"
 
-ML {*
-  Addsimprocs [Abel_Cancel.sum_conv, Abel_Cancel.rel_conv];
-*}
+simproc_setup abel_cancel_sum
+  ("a + b::'a::ab_group_add" | "a - b::'a::ab_group_add") =
+  {* fn phi => Abel_Cancel.sum_proc *}
+
+simproc_setup abel_cancel_relation
+  ("a < (b::'a::ordered_ab_group_add)" | "a \<le> (b::'a::ordered_ab_group_add)" | "c = (d::'b::ab_group_add)") =
+  {* fn phi => Abel_Cancel.rel_proc *}
 
 class linordered_ab_semigroup_add =
   linorder + ordered_ab_semigroup_add
@@ -1223,4 +1223,9 @@
 code_modulename Haskell
   Groups Arith
 
+
+text {* Legacy *}
+
+lemmas diff_def = diff_minus
+
 end