equal
deleted
inserted
replaced
31 similarly to auto_tac, but is aimed to solve the given subgoal totally. |
31 similarly to auto_tac, but is aimed to solve the given subgoal totally. |
32 |
32 |
33 * added option_map_eq_Some to simpset(), option_map_eq_Some RS iffD1 to claset() |
33 * added option_map_eq_Some to simpset(), option_map_eq_Some RS iffD1 to claset() |
34 * New directory HOL/UNITY: Chandy and Misra's UNITY formalism |
34 * New directory HOL/UNITY: Chandy and Misra's UNITY formalism |
35 |
35 |
36 * split_all_tac is now much faster and fails if there is nothing to split |
36 * split_all_tac is now much faster and fails if there is nothing to split. |
|
37 Existing (fragile) proofs may require adaption because the order and the names |
|
38 of the automatically generated variables have changed. |
37 split_all_tac has moved within claset() from usafe wrappers to safe wrappers, |
39 split_all_tac has moved within claset() from usafe wrappers to safe wrappers, |
38 which means that !!-bound variables are splitted much more aggressively. |
40 which means that !!-bound variables are splitted much more aggressively. |
39 If this splitting is not appropriate, use delSWrapper "split_all_tac". |
41 If this splitting is not appropriate, use delSWrapper "split_all_tac". |
40 |
42 |
41 * added disj_not1 = "(~P | Q) = (P --> Q)" to the default simpset |
43 * added disj_not1 = "(~P | Q) = (P --> Q)" to the default simpset |