isabelle: src/HOL/ex/IntRingDefs.ML@e2ecfd8622ae (annotated)

5601 b6456ccd9e3e revised for new treatment of integers paulson parents: 5227 diff changeset	1	(* Title: HOL/ex/IntRingDefs.thy
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	2	ID: $Id$
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	3	Author: Tobias Nipkow and Markus Wenzel
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	4	Copyright 1996 TU Muenchen
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	5	*)
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	6
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	7	Goalw [zero_int_def,zdiff_def] "(zero-x)+(x::int) = zero";
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	8	by (Simp_tac 1);
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	9	qed "left_inv_int";
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	10
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	11	Goalw [zero_int_def,zdiff_def] "x-y = (x::int) + (zero-y)";
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	12	by (Simp_tac 1);
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	13	qed "minus_inv_int";