src/HOL/Tools/res_clause.ML
changeset 19277 f7602e74d948
parent 19233 77ca20b0ed77
child 19354 aebf9dddccd7
     1.1 --- a/src/HOL/Tools/res_clause.ML	Thu Mar 16 20:19:25 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Fri Mar 17 09:34:23 2006 +0100
     1.3 @@ -90,8 +90,8 @@
     1.4  (*Provide readable names for the more common symbolic functions*)
     1.5  val const_trans_table =
     1.6        Symtab.make [("op =", "equal"),
     1.7 -	  	   ("op <=", "lessequals"),
     1.8 -		   ("op <", "less"),
     1.9 +	  	   ("Orderings.less_eq", "lessequals"),
    1.10 +		   ("Orderings.less", "less"),
    1.11  		   ("op &", "and"),
    1.12  		   ("op |", "or"),
    1.13  		   ("HOL.plus", "plus"),