* Pure: changed syntax of local blocks from {{ }} to { };
authorwenzelm
Mon May 22 16:03:43 2000 +0200 (2000-05-22)
changeset 89217c04c98132c4
parent 8920 af5e09b6c208
child 8922 490637ba1d7f
* Pure: changed syntax of local blocks from {{ }} to { };
* Pure: syntax of sorts made inner, i.e. have to write "{a, b, c}";
NEWS
     1.1 --- a/NEWS	Mon May 22 13:29:21 2000 +0200
     1.2 +++ b/NEWS	Mon May 22 16:03:43 2000 +0200
     1.3 @@ -35,6 +35,8 @@
     1.4  Lfp, Gfp, WF); this only affects ML packages that refer to const names
     1.5  internally;
     1.6  
     1.7 +* Isar: changed syntax of local blocks from {{ }} to { };
     1.8 +
     1.9  * ML: PureThy.add_thms/add_axioms/add_defs return theorems as well;
    1.10  
    1.11  * LaTeX: several improvements of isabelle.sty;
    1.12 @@ -72,6 +74,11 @@
    1.13  certain proof methods; internally, case names are attached to theorems
    1.14  as "tags";
    1.15  
    1.16 +* Pure: changed syntax of local blocks from {{ }} to { };
    1.17 +
    1.18 +* Pure: syntax of sorts made inner, i.e. have to write "{a, b, c}"
    1.19 +instead of {a, b, c};
    1.20 +
    1.21  * Pure now provides its own version of intro/elim/dest attributes;
    1.22  useful for building new logics, but beware of confusion with the
    1.23  Provers/classical ones;