diff -r d6d22254aeb7 -r 0fd03936dedb Attic/Quot/Quotient.thy --- a/Attic/Quot/Quotient.thy Tue Mar 16 17:20:46 2010 +0100 +++ b/Attic/Quot/Quotient.thy Tue Mar 16 18:02:08 2010 +0100 @@ -3,7 +3,7 @@ *) theory Quotient -imports Plain ATP_Linkup +imports Plain ATP_Linkup uses ("quotient_info.ML") ("quotient_typ.ML")