12 names in bold, underline etc. or colors; |
12 names in bold, underline etc. or colors; |
13 |
13 |
14 * HOLCF changes: derived all rules and arities |
14 * HOLCF changes: derived all rules and arities |
15 + axiomatic type classes instead of classes |
15 + axiomatic type classes instead of classes |
16 + typedef instead of faking type definitions |
16 + typedef instead of faking type definitions |
17 + eliminated the initernal constants less_fun, less_cfun, UU_fun, UU_cfun etc. |
17 + eliminated the internal constants less_fun, less_cfun, UU_fun, UU_cfun etc. |
18 + new axclasses cpo, chfin, flat with flat < chfin < pcpo < cpo < po |
18 + new axclasses cpo, chfin, flat with flat < chfin < pcpo < cpo < po |
19 + eliminated the types void, one, tr |
19 + eliminated the types void, one, tr |
20 + use unit lift and bool lift (with translations) instead of one and tr |
20 + use unit lift and bool lift (with translations) instead of one and tr |
21 + eliminated blift from Lift3.thy (use Def instead of blift) |
21 + eliminated blift from Lift3.thy (use Def instead of blift) |
22 all eliminated rules are derivd as theorems --> no visible changes |
22 all eliminated rules are derived as theorems --> no visible changes |
23 |
23 |
24 * simplifier: new functions delcongs, deleqcongs, and Delcongs. richer rep_ss. |
24 * simplifier: new functions delcongs, deleqcongs, and Delcongs. richer rep_ss. |
25 |
25 |
26 * simplifier: the solver is now split into a safe and an unsafe part. |
26 * simplifier: the solver is now split into a safe and an unsafe part. |
27 This should be invisible for the normal user, except that the |
27 This should be invisible for the normal user, except that the |
28 functions setsolver and addsolver have been renamed to setSolver and |
28 functions setsolver and addsolver have been renamed to setSolver and |
29 addSolver. added safe_asm_full_simp_tac. |
29 addSolver. added safe_asm_full_simp_tac. |
30 |
30 |
31 * classical reasoner: little changes in semantics of addafter (now: |
31 * classical reasoner: substitution with equality assumptions no longer |
32 addaltern), renamed setwrapper to setWrapper, addwrapper to addWrapper |
32 permutes other assumptions. |
|
33 |
|
34 * classical reasoner: minor changes in semantics of addafter (now called |
|
35 addaltern); renamed setwrapper to setWrapper and addwrapper to addWrapper; |
33 added safe wrapper (and access functions for it) |
36 added safe wrapper (and access functions for it) |
34 |
37 |
35 * improved combination of classical reasoner and simplifier: new |
38 * improved combination of classical reasoner and simplifier: new |
36 addss, auto_tac, functions for handling clasimpsets, ... Now, the |
39 addss, auto_tac, functions for handling clasimpsets, ... Now, the |
37 simplification is safe (therefore moved to safe_step_tac) and thus |
40 simplification is safe (therefore moved to safe_step_tac) and thus |
38 more complete, as multiple instantiation of unknowns (with slow_tac) |
41 more complete, as multiple instantiation of unknowns (with slow_tac). |
39 possible COULD MAKE EXISTING PROOFS FAIL; in case of problems with |
42 COULD MAKE EXISTING PROOFS FAIL; in case of problems with |
40 unstable old proofs: use unsafe_addss and unsafe_auto_tac |
43 old proofs, use unsafe_addss and unsafe_auto_tac |
41 |
44 |
42 * HOL: primrec now also works with type nat; |
45 * HOL: primrec now also works with type nat; |
43 |
46 |
44 * HOL: the constant for negation has been renamed from "not" to "Not" to |
47 * HOL: the constant for negation has been renamed from "not" to "Not" to |
45 harmonize with FOL, ZF, LK, etc. |
48 harmonize with FOL, ZF, LK, etc. |
53 |
56 |
54 * now supports alternative (named) syntax tables (parser and pretty |
57 * now supports alternative (named) syntax tables (parser and pretty |
55 printer); internal interface is provided by add_modesyntax(_i); |
58 printer); internal interface is provided by add_modesyntax(_i); |
56 |
59 |
57 * Pure, FOL, ZF, HOL, HOLCF now support symbolic input and output; to |
60 * Pure, FOL, ZF, HOL, HOLCF now support symbolic input and output; to |
58 be used in conjunction with the isabelle symbol font; uses the |
61 be used in conjunction with the Isabelle symbol font; uses the |
59 "symbols" syntax table; |
62 "symbols" syntax table; |
60 |
63 |
61 * infixes may now be declared with names independent of their syntax; |
64 * infixes may now be declared with names independent of their syntax; |
62 |
65 |
63 * added typed_print_translation (like print_translation, but may |
66 * added typed_print_translation (like print_translation, but may |