equal
deleted
inserted
replaced
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 |