2013-08-12 traytel temporary sorry's for temporarily nonterminating (due to 2b430bbb5a1a) proofs
2013-08-12 blanchet qualify intermediate typedefs
2013-08-12 blanchet avoid double qualification for case constants
2013-08-12 blanchet qualify more generated names with optional type name component
2013-08-12 traytel eliminated bogus assumption from theorem (that was instantiated with refl and resulted in flexflex pairs)
2013-08-12 traytel generalized library function
2013-08-12 wenzelm updated keywords;
2013-08-12 wenzelm merged
2013-08-12 wenzelm clarified Query_Operation.register: avoid hard-wired parallel policy;
2013-08-12 wenzelm moved generic module to its proper place;
2013-08-12 wenzelm manage hyperlinks via PIDE editor interface;
2013-08-12 wenzelm tuned whitespace;
2013-08-12 wenzelm prefer PIDE editor operations;
2013-08-12 wenzelm central management of Document.Overlays, independent of Document_Model;
2013-08-12 wenzelm tuned -- use Multi_Map;
2013-08-12 wenzelm support for maps with multiple entries per key;
2013-08-12 wenzelm tuned signature;
2013-08-12 wenzelm tuned signature;
2013-08-12 wenzelm tuned signature;
2013-08-12 wenzelm tuned signature -- more abstract PIDE editor operations;
2013-08-12 blanchet tuned messages
2013-08-12 blanchet clarified option name (since case/fold/rec are also destructors)
2013-08-12 blanchet define case constant from other 'free constructor' axioms
2013-08-12 blanchet introduced case tactics
2013-08-12 blanchet tuning
2013-08-12 blanchet handle both TVars and TFrees -- necessary for 'wrap_free_constructors'
2013-08-12 blanchet qualify map and rel names
2013-08-12 blanchet reverted ill-advised naming scheme of 5a77edcdbe54
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -28 +28 +50 +100 +300 +1000 +3000 +10000 tip