Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Restored warning comment
authorpaulson
Fri, 28 Jun 1996 11:10:32 +0200
changeset 1835 07eee14f5bd4
parent 1834 c780a4f39454
child 1836 861e29c7cada
Restored warning comment
src/Pure/logic.ML file | annotate | diff | comparison | revisions 
--- 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)
isabelle