src/HOL/Quotient.thy
changeset 45680 a61510361b89
parent 44921 58eef4843641
child 45782 f82020ca3248
     1.1 --- a/src/HOL/Quotient.thy	Tue Nov 29 21:50:00 2011 +0100
     1.2 +++ b/src/HOL/Quotient.thy	Tue Nov 29 22:45:21 2011 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  imports Plain Hilbert_Choice Equiv_Relations
     1.5  uses
     1.6    ("Tools/Quotient/quotient_info.ML")
     1.7 -  ("Tools/Quotient/quotient_typ.ML")
     1.8 +  ("Tools/Quotient/quotient_type.ML")
     1.9    ("Tools/Quotient/quotient_def.ML")
    1.10    ("Tools/Quotient/quotient_term.ML")
    1.11    ("Tools/Quotient/quotient_tacs.ML")
    1.12 @@ -696,7 +696,7 @@
    1.13  
    1.14  
    1.15  text {* Definitions of the quotient types. *}
    1.16 -use "Tools/Quotient/quotient_typ.ML"
    1.17 +use "Tools/Quotient/quotient_type.ML"
    1.18  
    1.19  
    1.20  text {* Definitions for quotient constants. *}