Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/IntRingDefs.ML
author paulson
Wed, 05 Aug 1998 10:57:25 +0200
changeset 5253 82a5ca6290aa
parent 5227 e5a6ace920a0
child 5601 b6456ccd9e3e
permissions -rw-r--r--
New record type of programs
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset 
     1
 
(*  Title:      HOL/Integ/IntRingDefs.thy
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";















isabelle