Tue, 05 Jul 2011 11:45:48 +0200clarified cancel_execution/await_cancellation;
wenzelm [Tue, 05 Jul 2011 11:45:48 +0200] rev 44541
clarified cancel_execution/await_cancellation;

Tue, 05 Jul 2011 11:16:37 +0200tuned signature;
wenzelm [Tue, 05 Jul 2011 11:16:37 +0200] rev 44540
tuned signature;
tuned;

Tue, 05 Jul 2011 10:54:05 +0200tuned;
wenzelm [Tue, 05 Jul 2011 10:54:05 +0200] rev 44539
tuned;

Tue, 05 Jul 2011 19:11:29 +0200rename lemma Infinite_Product_Measure.sigma_sets_subseteq, it hides Sigma_Algebra.sigma_sets_subseteq
hoelzl [Tue, 05 Jul 2011 19:11:29 +0200] rev 44538
rename lemma Infinite_Product_Measure.sigma_sets_subseteq, it hides Sigma_Algebra.sigma_sets_subseteq

Tue, 05 Jul 2011 17:09:59 +0100improved translation of lambdas in THF
nik [Tue, 05 Jul 2011 17:09:59 +0100] rev 44537
improved translation of lambdas in THF

Tue, 05 Jul 2011 17:09:59 +0100added generation of lambdas in THF
nik [Tue, 05 Jul 2011 17:09:59 +0100] rev 44536
added generation of lambdas in THF

Tue, 05 Jul 2011 17:09:59 +0100add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order)
nik [Tue, 05 Jul 2011 17:09:59 +0100] rev 44535
add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order)

Tue, 05 Jul 2011 09:54:39 +0200re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target
krauss [Tue, 05 Jul 2011 09:54:39 +0200] rev 44534
re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target

Mon, 04 Jul 2011 22:25:33 +0200Document.no_id/new_id as in ML (new_id *could* be session-specific but it isn't right now);
wenzelm [Mon, 04 Jul 2011 22:25:33 +0200] rev 44533
Document.no_id/new_id as in ML (new_id *could* be session-specific but it isn't right now);

Mon, 04 Jul 2011 22:11:32 +0200quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm [Mon, 04 Jul 2011 22:11:32 +0200] rev 44532
quasi-static Isabelle_System -- reduced tendency towards "functorial style";