author | wenzelm |

Wed Jun 13 11:54:03 2007 +0200 (2007-06-13) | |

changeset 23369 | 227c51012cdb |

parent 23368 | ad690b9bca1c |

child 23370 | 513a8ee192f1 |

* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;

* Isar: implicit use of prems from the Isar proof context is considered a legacy feature;

* Isar: implicit use of prems from the Isar proof context is considered a legacy feature;

1.1 --- a/NEWS Wed Jun 13 11:16:24 2007 +0200 1.2 +++ b/NEWS Wed Jun 13 11:54:03 2007 +0200 1.3 @@ -154,6 +154,21 @@ 1.4 Command 'print_theory' outputs the normalized system of recursive 1.5 equations, see section "definitions". 1.6 1.7 +* Isar: method "assumption" (and implicit closing of subproofs) now 1.8 +takes simple non-atomic goal assumptions into account: after applying 1.9 +an assumption as a rule the resulting subgoals are solved by atomic 1.10 +assumption steps. This is particularly useful to finish 'obtain' 1.11 +goals, such as "!!x. (!!x. P x ==> thesis) ==> P x ==> thesis", 1.12 +without referring to the original premise "!!x. P x ==> thesis" in the 1.13 +Isar proof context. POTENTIAL INCOMPATIBILITY: method "assumption" is 1.14 +more permissive. 1.15 + 1.16 +* Isar: implicit use of prems from the Isar proof context is 1.17 +considered a legacy feature. Common applications like ``have A .'' 1.18 +may be replaced by ``have A by fact'' or ``note `A`''. In general, 1.19 +referencing facts explicitly here improves readability and 1.20 +maintainability of proof texts. 1.21 + 1.22 * Isar: improper proof element 'guess' is like 'obtain', but derives 1.23 the obtained context from the course of reasoning! For example: 1.24