It is possible to enter type variables distinguished only by sort
constraint on the Isar level:
lemma
assumes P TYPE('a::order) and Q TYPE('a::group_add)
shows R TYPE('a::power)
using assms proof -
It is not clear to me whether this his always been possible that way or
slipped in due to some
Am 26.05.2010 um 18:54 schrieb Makarius:
* Some tuning of the Poly/ML runtime to shorted the (busy) wait interval
for external processes from 100ms to 10ms. This improves reactivity
of the ML bash/bash_output functions, at the cost of burning a few
extra cycles.
That is excellent
