diff -r 71043526295f -r 7b5ea59c0275 src/HOL/ex/IntRingDefs.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/IntRingDefs.ML	Thu Jun 25 13:57:34 1998 +0200
@@ -0,0 +1,16 @@
+(*  Title:      HOL/Integ/IntRingDefs.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow and Markus Wenzel
+    Copyright   1996 TU Muenchen
+
+*)
+
+open IntRingDefs;
+
+Goalw [zero_int_def,zdiff_def] "(zero-x)+(x::int) = zero";
+by (Simp_tac 1);
+qed "left_inv_int";
+
+Goalw [zero_int_def,zdiff_def] "x-y = (x::int) + (zero-y)";
+by (Simp_tac 1);
+qed "minus_inv_int";