NEWS
changeset 5046 de5eacb7361a
parent 5044 59808d00ea8d
child 5047 585fa380df1a
equal deleted inserted replaced
5045:a19e5c91a1ab 5046:de5eacb7361a
    35 commands.
    35 commands.
    36 
    36 
    37 * inductive definitions now handle disjunctive premises correctly (HOL
    37 * inductive definitions now handle disjunctive premises correctly (HOL
    38 and ZF);
    38 and ZF);
    39 
    39 
    40 * new toplevel commands 'thm' and 'thms' for retrieving theorems from
    40 * new toplevel commands 'Thm' and 'Thms' for retrieving theorems from
    41 the current theory context;
    41 the current theory context;
    42 
    42 
    43 * new theory section 'nonterminals';
    43 * new theory section 'nonterminals';
    44 
    44 
    45 * new theory section 'setup';
    45 * new theory section 'setup';