NEWS
changeset 9937 431c96ac997e
parent 9908 7c7ff65b6846
child 9941 fe05af7ec816
equal deleted inserted replaced
9936:f080397656d8 9937:431c96ac997e
    52 
    52 
    53 * ZF: new treatment of arithmetic (nat & int) may break some old proofs;
    53 * ZF: new treatment of arithmetic (nat & int) may break some old proofs;
    54 
    54 
    55 * Isar/Provers: intro/elim/dest attributes: changed
    55 * Isar/Provers: intro/elim/dest attributes: changed
    56 intro/intro!/intro!!  flags to intro!/intro/intro? (in most cases, one
    56 intro/intro!/intro!!  flags to intro!/intro/intro? (in most cases, one
    57 should have to change intro!! to intro? only);
    57 should have to change intro!! to intro? only); replaced "delrule" by
       
    58 "rule del";
    58 
    59 
    59 * Isar: changed syntax of local blocks from {{ }} to { };
    60 * Isar: changed syntax of local blocks from {{ }} to { };
    60 
    61 
    61 * Isar: renamed 'RS' attribute to 'THEN';
    62 * Isar: renamed 'RS' attribute to 'THEN';
    62 
    63 
   191 'inductive_cases' command and 'ind_cases' method; NOTE: use (cases
   192 'inductive_cases' command and 'ind_cases' method; NOTE: use (cases
   192 (simplified)) method in proper proofs;
   193 (simplified)) method in proper proofs;
   193 
   194 
   194 * Provers: intro/elim/dest attributes: changed intro/intro!/intro!!
   195 * Provers: intro/elim/dest attributes: changed intro/intro!/intro!!
   195 flags to intro!/intro/intro? (in most cases, one should have to change
   196 flags to intro!/intro/intro? (in most cases, one should have to change
   196 intro!! to intro? only);
   197 intro!! to intro? only); replaced "delrule" by "rule del";
   197 
   198 
   198 * names of theorems etc. may be natural numbers as well;
   199 * names of theorems etc. may be natural numbers as well;
   199 
   200 
   200 * 'pr' command: optional arguments for goals_limit and
   201 * 'pr' command: optional arguments for goals_limit and
   201 ProofContext.prems_limit; no longer prints theory contexts, but only
   202 ProofContext.prems_limit; no longer prints theory contexts, but only