Summary
- merged
- backed out changeset 1b8858f4c393: odd problems e.g. in CAVA_LTL_Modelchecker;
- more careful treatment of implicit context;
- clarified signature; more careful treatment of implicit context;
- more robust and convenient treatment of implicit context;
- clarified context: proper transfer;
- tuned;
- clarified modules: more direct data implementation;
- Added Takeuchi function to HOL-ex