Sun, 03 Mar 2013 14:29:30 +0100 uniform treatment of global/local proofs;
wenzelm [Sun, 03 Mar 2013 14:29:30 +0100] rev 51324
uniform treatment of global/local proofs; tuned;
Sun, 03 Mar 2013 13:57:03 +0100 tuned;
wenzelm [Sun, 03 Mar 2013 13:57:03 +0100] rev 51323
tuned;
Sun, 03 Mar 2013 13:43:57 +0100 clarified Toplevel.element_result wrt. Toplevel.is_ignored;
wenzelm [Sun, 03 Mar 2013 13:43:57 +0100] rev 51322
clarified Toplevel.element_result wrt. Toplevel.is_ignored;
Sun, 03 Mar 2013 13:23:06 +0100 more Thy_Syntax.element operations;
wenzelm [Sun, 03 Mar 2013 13:23:06 +0100] rev 51321
more Thy_Syntax.element operations;
Fri, 01 Mar 2013 22:15:31 +0100 coercion-invariant arguments at work
traytel [Fri, 01 Mar 2013 22:15:31 +0100] rev 51320
coercion-invariant arguments at work
Fri, 01 Mar 2013 22:15:31 +0100 constants with coercion-invariant arguments (possibility to disable/reenable
traytel [Fri, 01 Mar 2013 22:15:31 +0100] rev 51319
constants with coercion-invariant arguments (possibility to disable/reenable coercions under certain constants, necessary for the forthcoming logically unspecified control structures for case translations)
Thu, 28 Feb 2013 21:11:07 +0100 simplified Proof.future_proof;
wenzelm [Thu, 28 Feb 2013 21:11:07 +0100] rev 51318
simplified Proof.future_proof;
Thu, 28 Feb 2013 18:35:31 +0100 provide explicit dummy names (cf. dfe469293eb4);
wenzelm [Thu, 28 Feb 2013 18:35:31 +0100] rev 51317
provide explicit dummy names (cf. dfe469293eb4);
Thu, 28 Feb 2013 17:38:35 +0100 discontinued empty name bindings in 'axiomatization';
wenzelm [Thu, 28 Feb 2013 17:38:35 +0100] rev 51316
discontinued empty name bindings in 'axiomatization';
Thu, 28 Feb 2013 17:14:55 +0100 provide common HOLogic.conj_conv and HOLogic.eq_conv;
wenzelm [Thu, 28 Feb 2013 17:14:55 +0100] rev 51315
provide common HOLogic.conj_conv and HOLogic.eq_conv;
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip