src/ZF/ex/Integ.thy
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 5507 2fd99b2d41e1
     1.1 --- a/src/ZF/ex/Integ.thy	Mon Feb 05 21:33:14 1996 +0100
     1.2 +++ b/src/ZF/ex/Integ.thy	Tue Feb 06 12:27:17 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	ZF/ex/integ.thy
     1.5 +(*  Title:      ZF/ex/integ.thy
     1.6      ID:         $Id$
     1.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.9      Copyright   1993  University of Cambridge
    1.10  
    1.11  The integers as equivalence classes over nat*nat.
    1.12 @@ -9,34 +9,34 @@
    1.13  Integ = EquivClass + Arith +
    1.14  consts
    1.15      intrel,integ::      i
    1.16 -    znat	::	i=>i		("$# _" [80] 80)
    1.17 -    zminus	::	i=>i		("$~ _" [80] 80)
    1.18 -    znegative	::	i=>o
    1.19 -    zmagnitude	::	i=>i
    1.20 +    znat        ::      i=>i            ("$# _" [80] 80)
    1.21 +    zminus      ::      i=>i            ("$~ _" [80] 80)
    1.22 +    znegative   ::      i=>o
    1.23 +    zmagnitude  ::      i=>i
    1.24      "$*"        ::      [i,i]=>i      (infixl 70)
    1.25      "$'/"       ::      [i,i]=>i      (infixl 70) 
    1.26      "$'/'/"     ::      [i,i]=>i      (infixl 70)
    1.27 -    "$+"	::      [i,i]=>i      (infixl 65)
    1.28 +    "$+"        ::      [i,i]=>i      (infixl 65)
    1.29      "$-"        ::      [i,i]=>i      (infixl 65)
    1.30 -    "$<"	:: 	[i,i]=>o  	(infixl 50)
    1.31 +    "$<"        ::      [i,i]=>o        (infixl 50)
    1.32  
    1.33  defs
    1.34  
    1.35      intrel_def
    1.36 -     "intrel == {p:(nat*nat)*(nat*nat). 		
    1.37 +     "intrel == {p:(nat*nat)*(nat*nat).                 
    1.38          EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
    1.39  
    1.40      integ_def   "integ == (nat*nat)/intrel"
    1.41      
    1.42 -    znat_def	"$# m == intrel `` {<m,0>}"
    1.43 +    znat_def    "$# m == intrel `` {<m,0>}"
    1.44      
    1.45 -    zminus_def	"$~ Z == UN <x,y>:Z. intrel``{<y,x>}"
    1.46 +    zminus_def  "$~ Z == UN <x,y>:Z. intrel``{<y,x>}"
    1.47      
    1.48      znegative_def
    1.49 -	"znegative(Z) == EX x y. x<y & y:nat & <x,y>:Z"
    1.50 +        "znegative(Z) == EX x y. x<y & y:nat & <x,y>:Z"
    1.51      
    1.52      zmagnitude_def
    1.53 -	"zmagnitude(Z) == UN <x,y>:Z. (y#-x) #+ (x#-y)"
    1.54 +        "zmagnitude(Z) == UN <x,y>:Z. (y#-x) #+ (x#-y)"
    1.55      
    1.56      (*Cannot use UN<x1,y2> here or in zmult because of the form of congruent2.
    1.57        Perhaps a "curried" or even polymorphic congruent predicate would be
    1.58 @@ -47,7 +47,7 @@
    1.59                             in intrel``{<x1#+x2, y1#+y2>}"
    1.60      
    1.61      zdiff_def   "Z1 $- Z2 == Z1 $+ zminus(Z2)"
    1.62 -    zless_def	"Z1 $< Z2 == znegative(Z1 $- Z2)"
    1.63 +    zless_def   "Z1 $< Z2 == znegative(Z1 $- Z2)"
    1.64      
    1.65      (*This illustrates the primitive form of definitions (no patterns)*)
    1.66      zmult_def