Fri, 23 Feb 2018 19:36:16 +0100 | wenzelm | prefer existing HOLogic.mk_obj_eq, despite subtle semantic differences of COMP vs. RS; | changeset | files |
Fri, 23 Feb 2018 19:25:37 +0100 | wenzelm | added HOLogic.mk_obj_eq convenience and eliminated some clones; | changeset | files |