NEWS
changeset 11657 03c4a5c08a79
parent 11633 c8945e0dc00b
child 11663 8a86409108fe
equal deleted inserted replaced
11656:e499dceca569 11657:03c4a5c08a79
    24 * Isar/HOL: 'inductive' now longer features separate (collective)
    24 * Isar/HOL: 'inductive' now longer features separate (collective)
    25 attributes for 'intros';
    25 attributes for 'intros';
    26 
    26 
    27 
    27 
    28 *** HOL ***
    28 *** HOL ***
       
    29 
       
    30 * HOL: linorder_less_split superseded by linorder_cases;
    29 
    31 
    30 * HOL: added "The" definite description operator; move Hilbert's "Eps"
    32 * HOL: added "The" definite description operator; move Hilbert's "Eps"
    31 to peripheral theory "Hilbert_Choice";
    33 to peripheral theory "Hilbert_Choice";
    32 
    34 
    33 * HOL: made split_all_tac safe; EXISTING PROOFS MAY FAIL OR LOOP, so
    35 * HOL: made split_all_tac safe; EXISTING PROOFS MAY FAIL OR LOOP, so
    66 
    68 
    67 * Meta-level proof terms (by Stefan Berghofer), see also ref manual;
    69 * Meta-level proof terms (by Stefan Berghofer), see also ref manual;
    68 
    70 
    69 * Classical reasoner: renamed addaltern to addafter, addSaltern to
    71 * Classical reasoner: renamed addaltern to addafter, addSaltern to
    70 addSafter;
    72 addSafter;
       
    73 
       
    74 * syntax: support non-oriented infixes;
    71 
    75 
    72 * print modes "type_brackets" and "no_type_brackets" control output of
    76 * print modes "type_brackets" and "no_type_brackets" control output of
    73 nested => (types); the default behavior is "brackets";
    77 nested => (types); the default behavior is "brackets";
    74 
    78 
    75 * system: support Poly/ML 4.1.1 (now able to manage large heaps);
    79 * system: support Poly/ML 4.1.1 (now able to manage large heaps);