| changeset 1835 | 07eee14f5bd4 |
| parent 1500 | b2de3b3277b8 |
| child 2266 | 82aef6857c5b |
--- a/src/Pure/logic.ML Thu Jun 27 15:24:17 1996 +0200 +++ b/src/Pure/logic.ML Fri Jun 28 11:10:32 1996 +0200 @@ -56,7 +56,7 @@ (** equality **) -(*Make an equality.*) +(*Make an equality. DOES NOT CHECK TYPE OF u*) fun mk_equals(t,u) = equals(fastype_of t) $ t $ u; fun dest_equals (Const("==",_) $ t $ u) = (t,u)