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 |
Fri, 23 Feb 2018 17:59:57 +0100 | wenzelm | tuned -- use existing Morphism.instantiate_morphism; | changeset | files |