NEWS
changeset 3697 c5833dfcc2cc
parent 3671 8326f03d667c
child 3715 6e074b41c735
equal deleted inserted replaced
3696:e2af92a3281b 3697:c5833dfcc2cc
     2 Isabelle NEWS -- history of user-visible changes
     2 Isabelle NEWS -- history of user-visible changes
     3 ================================================
     3 ================================================
     4 
     4 
     5 New in Isabelle???? (DATE ????)
     5 New in Isabelle???? (DATE ????)
     6 -------------------------------
     6 -------------------------------
       
     7 
       
     8 * Pure: fixed idt/idts vs. pttrn/pttrns syntactic categories;
       
     9 
       
    10 * HOLCF: fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
     7 
    11 
     8 * added extended adm_tac to simplifier in HOLCF. Is now capable to discharge
    12 * added extended adm_tac to simplifier in HOLCF. Is now capable to discharge
     9   adm (%x. P (t x)), where P is chainfinite and t continuous.
    13   adm (%x. P (t x)), where P is chainfinite and t continuous.
    10 
    14 
    11 * replaced print_goals_ref hook by print_current_goals_fn and
    15 * replaced print_goals_ref hook by print_current_goals_fn and