src/HOL/ex/IntRingDefs.ML

New example

(*  Title:      HOL/ex/IntRingDefs.thy
    ID:         $Id$
    Author:     Tobias Nipkow and Markus Wenzel
    Copyright   1996 TU Muenchen
*)

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";