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.
Removed spurious comment about eq_cs
authorlcp
Thu, 12 Jan 1995 03:02:34 +0100
changeset 854 2e3ca37dfa14
parent 853 a4b286dfdd6f
child 855 4c8d0ece1f95
Removed spurious comment about eq_cs
src/ZF/ZF.ML file | annotate | diff | comparison | revisions 
--- a/src/ZF/ZF.ML	Thu Jan 12 03:02:05 1995 +0100
+++ b/src/ZF/ZF.ML	Thu Jan 12 03:02:34 1995 +0100
@@ -411,7 +411,6 @@
     swap_res_tac [minor] 1,
     assume_tac 1 ]);
 
-(*Can replace most uses by eq_cs (which is ZF_cs addSIs [equalityI])*)
 (*A claset that leaves <= formulae unchanged!*)
 val subset0_cs = FOL_cs
   addSIs [ballI, InterI, CollectI, PowI, empty_subsetI]
isabelle