isabelle: src/HOL/Integ/IntRingDefs.ML@e00c13a29eda (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";
e00c13a29eda Ring Theory. nipkow parents: diff changeset	11	by(Simp_tac 1);
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)";
e00c13a29eda Ring Theory. nipkow parents: diff changeset	15	by(Simp_tac 1);
e00c13a29eda Ring Theory. nipkow parents: diff changeset	16	qed "minus_inv_int";