| author | paulson |
| Fri, 11 Sep 1998 16:25:40 +0200 | |
| changeset 5479 | 5a5dfb0f0d7d |
| parent 5227 | e5a6ace920a0 |
| child 5601 | b6456ccd9e3e |
| permissions | -rw-r--r-- |
(* Title: HOL/Integ/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";