src/HOL/Quotient.thy
changeset 35827 f552152d7747
parent 35294 0e1adc24722f
child 36116 a6eab3be095b
     1.1 --- a/src/HOL/Quotient.thy	Wed Mar 17 19:26:05 2010 +0100
     1.2 +++ b/src/HOL/Quotient.thy	Wed Mar 17 19:37:44 2010 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Definition of Quotient Types *}
     1.5  
     1.6  theory Quotient
     1.7 -imports Plain ATP_Linkup
     1.8 +imports Plain Sledgehammer
     1.9  uses
    1.10    ("~~/src/HOL/Tools/Quotient/quotient_info.ML")
    1.11    ("~~/src/HOL/Tools/Quotient/quotient_typ.ML")