2013-04-10 traytel declaration attribute for case combinators
2013-04-09 berghofe Handle dummy patterns in parse translation rather than check phase
2013-04-05 traytel disallow coercions to interfere with case translations
2013-04-05 traytel allow redundant cases in the list comprehension translation
2013-04-05 traytel recur in the expression to be matched (do not rely on repetitive execution of a check phase);
2013-04-05 traytel tuned whitespace
2013-04-04 berghofe Use Type.raw_match instead of Sign.typ_match
2013-04-05 traytel special constant to prevent eta-contraction of the check-phase syntax of case translations
2013-01-22 traytel separate data used for case translation from the datatype package
2013-01-22 berghofe case translations performed in a separate check phase (with adjustments by traytel)
2013-04-10 wenzelm formal proof context for axclass proofs;
2013-04-10 wenzelm prefer local context;
2013-04-10 wenzelm proper proof context;
2013-04-10 wenzelm tuned;
2013-04-09 wenzelm merged
2013-04-09 wenzelm add command timings (like document command status);
2013-04-09 wenzelm tuned signature;
2013-04-09 wenzelm public Isabelle_Process.xml_cache (thread-safe);
2013-04-09 wenzelm tuned signature;
2013-04-09 wenzelm just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
2013-04-09 wenzelm clarified protocol_message undefinedness;
2013-04-09 wenzelm quote by Alan Kay;
2013-04-09 wenzelm more accurate documentation;
2013-04-09 wenzelm discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
2013-04-09 wenzelm more accurate documentation of "(structure)" mixfix;
2013-04-09 wenzelm more robust static structure reference, avoid dynamic Proof_Context.intern_skolem in Syntax_Phases.decode_term;
2013-04-09 wenzelm tuned comment;
2013-04-09 wenzelm just one syntax category "mixfix" -- check structure annotation semantically;
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -28 +28 +50 +100 +300 +1000 +3000 +10000 +30000 tip