isabelle: src/HOL/Integ/IntRingDefs.ML@74a12e86b20b (annotated)

2281 e00c13a29eda Ring Theory. nipkow parents: diff changeset	1	(* Title: HOL/Integ/IntRingDefs.thy
e00c13a29eda Ring Theory. nipkow parents: diff changeset	2	ID: $Id$
e00c13a29eda Ring Theory. nipkow parents: diff changeset	3	Author: Tobias Nipkow and Markus Wenzel
e00c13a29eda Ring Theory. nipkow parents: diff changeset	4	Copyright 1996 TU Muenchen
e00c13a29eda Ring Theory. nipkow parents: diff changeset	5
e00c13a29eda Ring Theory. nipkow parents: diff changeset	6	*)
e00c13a29eda Ring Theory. nipkow parents: diff changeset	7
e00c13a29eda Ring Theory. nipkow parents: diff changeset	8	open IntRingDefs;
e00c13a29eda Ring Theory. nipkow parents: diff changeset	9
e00c13a29eda Ring Theory. nipkow parents: diff changeset	10	goalw thy [zero_int_def,zdiff_def] "(zero-x)+(x::int) = zero";
4423 a129b817b58a expandshort; wenzelm parents: 2281 diff changeset	11	by (Simp_tac 1);
2281 e00c13a29eda Ring Theory. nipkow parents: diff changeset	12	qed "left_inv_int";
e00c13a29eda Ring Theory. nipkow parents: diff changeset	13
e00c13a29eda Ring Theory. nipkow parents: diff changeset	14	goalw thy [zero_int_def,zdiff_def] "x-y = (x::int) + (zero-y)";
4423 a129b817b58a expandshort; wenzelm parents: 2281 diff changeset	15	by (Simp_tac 1);
2281 e00c13a29eda Ring Theory. nipkow parents: diff changeset	16	qed "minus_inv_int";