*** empty log message ***
authorslotosch
Fri Apr 04 16:16:35 1997 +0200 (1997-04-04)
changeset 2910905aa895136c
parent 2909 22a8a97b66be
child 2911 8a680e310f04
*** empty log message ***
src/HOL/Quot/FRACT.thy
src/HOL/Quot/README
     1.1 --- a/src/HOL/Quot/FRACT.thy	Fri Apr 04 16:04:28 1997 +0200
     1.2 +++ b/src/HOL/Quot/FRACT.thy	Fri Apr 04 16:16:35 1997 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4      Author:     Oscar Slotosch
     1.5      Copyright   1997 Technische Universitaet Muenchen
     1.6  
     1.7 -Example for higher order quotients: fractionals
     1.8 +Example for higher order quotients: fractions
     1.9  *)
    1.10  
    1.11  FRACT = NPAIR + HQUOT +
     2.1 --- a/src/HOL/Quot/README	Fri Apr 04 16:04:28 1997 +0200
     2.2 +++ b/src/HOL/Quot/README	Fri Apr 04 16:16:35 1997 +0200
     2.3 @@ -7,7 +7,7 @@
     2.4  Quotients are a specialization of higher order quotients.
     2.5  The use the same constructor quot with the subclass er.
     2.6  
     2.7 -An Example for the application of quotients are the fractional numbers.
     2.8 +An Example for the application of quotients are the fractions.
     2.9  The example shows how to define an equivalence relation and how to use
    2.10  the quotients.
    2.11