NEWS
changeset 3042 21cd332b65d3
parent 3006 8a1eb4531fbb
child 3107 492a3d5d2b17
equal deleted inserted replaced
3041:bdd21deed6ea 3042:21cd332b65d3
    84 addSolver.  added safe_asm_full_simp_tac.
    84 addSolver.  added safe_asm_full_simp_tac.
    85 
    85 
    86 
    86 
    87 *** HOL ***
    87 *** HOL ***
    88 
    88 
       
    89 * a generic induction tactic `induct_tac' which works for all datatypes and
       
    90 also for type `nat'.
       
    91 
    89 * patterns in case expressions allow tuple patterns as arguments to
    92 * patterns in case expressions allow tuple patterns as arguments to
    90 constructors, for example `case x of [] => ... | (x,y,z)#ps => ...'
    93 constructors, for example `case x of [] => ... | (x,y,z)#ps => ...'
    91 
    94 
    92 * primrec now also works with type nat;
    95 * primrec now also works with type nat;
    93 
    96