equal
deleted
inserted
replaced
18 setWrapper, setSWrapper, compWrapper and compSWrapper are replaced by |
18 setWrapper, setSWrapper, compWrapper and compSWrapper are replaced by |
19 addWrapper, addSWrapper: claset * wrapper -> claset |
19 addWrapper, addSWrapper: claset * wrapper -> claset |
20 delWrapper, delSWrapper: claset * string -> claset |
20 delWrapper, delSWrapper: claset * string -> claset |
21 getWrapper is renamed to appWrappers, getSWrapper to appSWrappers; |
21 getWrapper is renamed to appWrappers, getSWrapper to appSWrappers; |
22 |
22 |
|
23 * Inductive definitions now handle disjunctive premises correctly (HOL and ZF) |
|
24 |
23 |
25 |
24 *** HOL *** |
26 *** HOL *** |
25 |
27 |
26 * added option_map_eq_Some to simpset(), option_map_eq_Some RS iffD1 to claset() |
28 * added option_map_eq_Some to simpset(), option_map_eq_Some RS iffD1 to claset() |
27 * New directory HOL/UNITY: Chandy and Misra's UNITY formalism |
29 * New directory HOL/UNITY: Chandy and Misra's UNITY formalism |
34 * HOL/Arithmetic: removed 'pred' (predecessor) function; and generalized |
36 * HOL/Arithmetic: removed 'pred' (predecessor) function; and generalized |
35 some theorems about n-1 |
37 some theorems about n-1 |
36 |
38 |
37 * HOL/Relation: renamed the relational operatotr r^-1 "converse" instead of |
39 * HOL/Relation: renamed the relational operatotr r^-1 "converse" instead of |
38 "inverse" |
40 "inverse" |
|
41 |
|
42 * HOL/equalities: added many new laws involving unions, intersectinos, |
|
43 difference, etc. |
|
44 |
|
45 * recdef can now declare non-recursive functions, with {} supplied as the |
|
46 well-founded relation |
39 |
47 |
40 * Simplifier: |
48 * Simplifier: |
41 |
49 |
42 -The rule expand_if is now part of the default simpset. This means that |
50 -The rule expand_if is now part of the default simpset. This means that |
43 the simplifier will eliminate all ocurrences of if-then-else in the |
51 the simplifier will eliminate all ocurrences of if-then-else in the |
58 old Asm_full_simp_tac in that it does not rotate premises. |
66 old Asm_full_simp_tac in that it does not rotate premises. |
59 |
67 |
60 * new theory Vimage (inverse image of a function, syntax f-``B); |
68 * new theory Vimage (inverse image of a function, syntax f-``B); |
61 |
69 |
62 * many new identities for unions, intersections, etc.; |
70 * many new identities for unions, intersections, etc.; |
63 |
|
64 |
71 |
65 |
72 |
66 New in Isabelle98 (January 1998) |
73 New in Isabelle98 (January 1998) |
67 -------------------------------- |
74 -------------------------------- |
68 |
75 |