src/HOL/Library/Fraction_Field.thy
changeset 35372 ca158c7b1144
parent 31998 2c7a24f74db9
child 36312 26eea417ccc4
     1.1 --- a/src/HOL/Library/Fraction_Field.thy	Wed Feb 24 14:19:54 2010 +0100
     1.2 +++ b/src/HOL/Library/Fraction_Field.thy	Wed Feb 24 14:34:40 2010 +0100
     1.3 @@ -1,12 +1,12 @@
     1.4 -(*  Title:      Fraction_Field.thy
     1.5 +(*  Title:      HOL/Library/Fraction_Field.thy
     1.6      Author:     Amine Chaieb, University of Cambridge
     1.7  *)
     1.8  
     1.9  header{* A formalization of the fraction field of any integral domain 
    1.10 -         A generalization of Rational.thy from int to any integral domain *}
    1.11 +         A generalization of Rat.thy from int to any integral domain *}
    1.12  
    1.13  theory Fraction_Field
    1.14 -imports Main (* Equiv_Relations Plain *)
    1.15 +imports Main
    1.16  begin
    1.17  
    1.18  subsection {* General fractions construction *}