summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Tue, 27 Aug 2002 10:59:21 +0200 | |

changeset 13522 | 934fffeb6f38 |

parent 13521 | 1aaa14d7a4b9 |

child 13523 | 079af5c90d1c |

* Isar: preview of problems to finish 'show' now produce an error

--- a/NEWS Sat Aug 24 18:53:43 2002 +0200 +++ b/NEWS Tue Aug 27 10:59:21 2002 +0200 @@ -1,3 +1,4 @@ + Isabelle NEWS -- history user-relevant changes ============================================== @@ -28,14 +29,17 @@ "foo" are split into "foo.hyps" (from the rule) and "foo.prems" (from the goal statement); "foo" still refers to all facts collectively; +* Isar: preview of problems to finish 'show' now produce an error +rather than just a warning (in interactive mode); + *** HOL *** * 'typedef' command has new option "open" to suppress the set definition; -* Functions Min and Max on finite sets have been introduced. - (theory Finite_Set) +* functions Min and Max on finite sets have been introduced (theory +Finite_Set); * attribute [symmetric] now works for relations as well; it turns (x,y) : R^-1 into (y,x) : R, and vice versa;