haftmann [Wed, 02 Aug 2017 20:33:39 +0200] rev 66310
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
sufficient to keep history stamps rather than complete historized data;
semantically conflicting specifications are temoprary blacklisted after theory merge but remain historized;
clarified signature;