summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

NEWS

changeset 10391 | 0025fd11882c |

parent 10337 | fca9cd9fd115 |

child 10401 | 58bb50f69497 |

--- a/NEWS Fri Nov 03 21:35:59 2000 +0100 +++ b/NEWS Sat Nov 04 18:39:44 2000 +0100 @@ -8,6 +8,8 @@ * HOL: contrapos, contrapos2 renamed to contrapos_nn, contrapos_pp; +* Isar: 'obtain' no longer declares "that" fact as simp/intro; + *** Document preparation *** @@ -24,10 +26,21 @@ into document output unless you really know what you are doing! - *** Isar *** -* HOL: default proof step now includes 'intro_classes'; +* Pure: assumption method (an implicit finishing) now handles actual +rules as well; + +* Pure: improved 'obtain' --- moved to Pure, insert "that" into +initial goal, declare "that" only as Pure intro (only for single +steps); the "that" rule assumption may now be involved in implicit +finishing, thus ".." becomes a feasible for trivial obtains; + +* Pure: default proof step now includes 'intro_classes'; thus trivial +instance proofs may be performed by ".."; + +* Pure: ?thesis / ?this / "..." now work for pure meta-level +statements as well; *** HOL *** @@ -38,6 +51,16 @@ HOL/Induct/Multiset, HOL/Induct/Acc (as Accessible_Part), HOL/While (as While_Combinator), HOL/Lex/Prefix (as List_Prefix); +* HOL/typedef: simplified package, provide more useful rules (see also +HOL/subset.thy); + + +*** General *** + +* Provers: fast_tac (and friends) now handle actual object-logic rules +as assumptions as well; + + New in Isabelle99-1 (October 2000) ----------------------------------