src/HOL/HOL.thy
changeset 13550 5a176b8dda84
parent 13456 42601eb7553f
child 13553 855f6bae851e
     1.1 --- a/src/HOL/HOL.thy	Thu Aug 29 16:15:11 2002 +0200
     1.2 +++ b/src/HOL/HOL.thy	Fri Aug 30 16:42:45 2002 +0200
     1.3 @@ -603,13 +603,6 @@
     1.4    "op <="       :: "['a::ord, 'a] => bool"             ("op \<le>")
     1.5    "op <="       :: "['a::ord, 'a] => bool"             ("(_/ \<le> _)"  [50, 51] 50)
     1.6  
     1.7 -(*Tell blast about overloading of < and <= to reduce the risk of
     1.8 -  its applying a rule for the wrong type*)
     1.9 -ML {*
    1.10 -Blast.overloaded ("op <" , domain_type);
    1.11 -Blast.overloaded ("op <=", domain_type);
    1.12 -*}
    1.13 -
    1.14  
    1.15  subsubsection {* Monotonicity *}
    1.16