author | wenzelm |

Tue Aug 27 10:59:21 2002 +0200 (2002-08-27) | |

changeset 13522 | 934fffeb6f38 |

parent 13521 | 1aaa14d7a4b9 |

child 13523 | 079af5c90d1c |

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

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