2553
|
1 |
|
|
2 |
Isabelle NEWS -- history of user-visible changes
|
|
3 |
================================================
|
|
4 |
|
2554
|
5 |
|
|
6 |
New in Isabelle94-8 (??????????? 1997 FIXME)
|
|
7 |
---------------------------------------
|
2553
|
8 |
|
|
9 |
* the NEWS file;
|
|
10 |
|
|
11 |
* new utilities to build / run / maintain Isabelle etc. (in parts
|
2555
|
12 |
still somewhat experimental); old Makefiles etc. still functional;
|
2553
|
13 |
|
|
14 |
* simplifier: termless order as parameter; added interface for
|
|
15 |
simplification procedures (functions that produce *proven* rewrite
|
|
16 |
rules on the fly, depending on current redex);
|
|
17 |
|
|
18 |
* now supports alternative (named) syntax tables (parser and pretty
|
|
19 |
printer); internal interface is provided by add_modesyntax(_i);
|
|
20 |
|
|
21 |
* Pure, FOL, ZF, HOL, HOLCF now support symbolic input and output; to
|
|
22 |
be used in conjunction with the isabelle symbol font; uses the
|
|
23 |
"symbols" syntax table;
|
|
24 |
|
|
25 |
* infixes may now be declared with names independent of their syntax;
|
|
26 |
|
2555
|
27 |
* added typed_print_translation (like print_translation, but may
|
|
28 |
access type of constant);
|
2553
|
29 |
|
|
30 |
* prlim command for dealing with lots of subgoals (an easier way of
|
|
31 |
setting goals_limit);
|
|
32 |
|
|
33 |
* HOL/ex/Ring.thy declares cring_simp, which solves equational
|
|
34 |
problems in commutative rings, using axiomatic type classes for + and *;
|
|
35 |
|
|
36 |
* ZF now has Fast_tac, Simp_tac and Auto_tac. WARNING: don't use
|
|
37 |
ZF.thy anymore! Contains fewer defs and could make a bogus simpset.
|
|
38 |
Beware of Union_iff. eq_cs is gone, can be put back as ZF_cs addSIs
|
|
39 |
[equalityI];
|
|
40 |
|
|
41 |
* more examples in HOL/MiniML and HOL/Auth;
|
|
42 |
|
|
43 |
* more default rewrite rules in HOL for quantifiers, union/intersection;
|
|
44 |
|
|
45 |
|
2554
|
46 |
|
2553
|
47 |
New in Isabelle94-7 (November 96)
|
|
48 |
---------------------------------
|
|
49 |
|
|
50 |
* allowing negative levels (as offsets) in prlev and choplev;
|
|
51 |
|
2554
|
52 |
* super-linear speedup for large simplifications;
|
|
53 |
|
|
54 |
* FOL, ZF and HOL now use miniscoping: rewriting pushes
|
|
55 |
quantifications in as far as possible (COULD MAKE EXISTING PROOFS
|
|
56 |
FAIL); can suppress it using the command Delsimps (ex_simps @
|
|
57 |
all_simps); De Morgan laws are also now included, by default;
|
|
58 |
|
|
59 |
* improved printing of ==> : ~:
|
|
60 |
|
|
61 |
* new object-logic "Sequents" adds linear logic, while replacing LK
|
|
62 |
and Modal (thanks to Sara Kalvala);
|
|
63 |
|
|
64 |
* HOL/Auth: correctness proofs for authentication protocols;
|
|
65 |
|
|
66 |
* HOL: new auto_tac combines rewriting and classical reasoning (many
|
|
67 |
examples on HOL/Auth);
|
|
68 |
|
|
69 |
* HOL: new command AddIffs for declaring theorems of the form P=Q to
|
|
70 |
the rewriter and classical reasoner simultaneously;
|
|
71 |
|
|
72 |
* function uresult no longer returns theorems in "standard" format;
|
|
73 |
regain previous version by: val uresult = standard o uresult;
|
|
74 |
|
|
75 |
|
|
76 |
|
|
77 |
New in Isabelle94-6
|
|
78 |
-------------------
|
|
79 |
|
|
80 |
* oracles -- these establish an interface between Isabelle and trusted
|
|
81 |
external reasoners, which may deliver results as theorems;
|
|
82 |
|
|
83 |
* proof objects (in particular record all uses of oracles);
|
|
84 |
|
|
85 |
* Simp_tac, Fast_tac, etc. that refer to implicit simpset / claset;
|
|
86 |
|
|
87 |
* "constdefs" section in theory files;
|
|
88 |
|
|
89 |
* "primrec" section (HOL) no longer requires names;
|
|
90 |
|
|
91 |
* internal type "tactic" now simply "thm -> thm Sequence.seq";
|
|
92 |
|
|
93 |
|
|
94 |
|
|
95 |
New in Isabelle94-5
|
|
96 |
-------------------
|
|
97 |
|
|
98 |
* reduced space requirements;
|
|
99 |
|
|
100 |
* automatic HTML generation from theories;
|
|
101 |
|
|
102 |
* theory files no longer require "..." (quotes) around most types;
|
|
103 |
|
|
104 |
* new examples, including two proofs of the Church-Rosser theorem;
|
|
105 |
|
|
106 |
* non-curried (1994) version of HOL is no longer distributed;
|
|
107 |
|
2553
|
108 |
|
|
109 |
$Id$
|