NEWS
changeset 2993 9e46778b97ab
parent 2971 c1e1e8406fb2
child 3002 223e5d65faaa
equal deleted inserted replaced
2992:395686b418a4 2993:9e46778b97ab
    45 simplification is safe (therefore moved to safe_step_tac) and thus
    45 simplification is safe (therefore moved to safe_step_tac) and thus
    46 more complete, as multiple instantiation of unknowns (with slow_tac).
    46 more complete, as multiple instantiation of unknowns (with slow_tac).
    47 COULD MAKE EXISTING PROOFS FAIL; in case of problems with
    47 COULD MAKE EXISTING PROOFS FAIL; in case of problems with
    48 old proofs, use unsafe_addss and unsafe_auto_tac
    48 old proofs, use unsafe_addss and unsafe_auto_tac
    49 
    49 
       
    50 * HOL: patterns in case expressions allow tuple patterns as arguments to
       
    51 constructors, for example `case x of [] => ... | (x,y,z)#ps => ...'
       
    52 
    50 * HOL: primrec now also works with type nat;
    53 * HOL: primrec now also works with type nat;
    51 
    54 
    52 * HOL: the constant for negation has been renamed from "not" to "Not" to
    55 * HOL: the constant for negation has been renamed from "not" to "Not" to
    53 harmonize with FOL, ZF, LK, etc.
    56 harmonize with FOL, ZF, LK, etc.
    54 
    57