src/ZF/Int_ZF.thy
changeset 32960 69916a850301
parent 26056 6a0801279f4c
child 41777 1f7cbe39d425
     1.1 --- a/src/ZF/Int_ZF.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/ZF/Int_ZF.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -1,8 +1,6 @@
     1.4  (*  Title:      ZF/Int.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7      Copyright   1993  University of Cambridge
     1.8 -
     1.9  *)
    1.10  
    1.11  header{*The Integers as Equivalence Classes Over Pairs of Natural Numbers*}
    1.12 @@ -55,7 +53,7 @@
    1.13    --{*could be replaced by an absolute value function from int to int?*}
    1.14      "zmagnitude(z) ==
    1.15       THE m. m\<in>nat & ((~ znegative(z) & z = $# m) |
    1.16 -		       (znegative(z) & $- z = $# m))"
    1.17 +                       (znegative(z) & $- z = $# m))"
    1.18  
    1.19  definition
    1.20    raw_zmult   ::      "[i,i]=>i"  where