equal
deleted
inserted
replaced
1 |
|
2 Isabelle NEWS -- history of user-visible changes |
1 Isabelle NEWS -- history of user-visible changes |
3 ================================================ |
2 ================================================ |
4 |
3 |
5 New in Isabelle???? (DATE ????) |
4 New in Isabelle???? (DATE ????) |
6 ------------------------------- |
5 ------------------------------- |
72 |
71 |
73 * Pure: fixed idt/idts vs. pttrn/pttrns syntactic categories; |
72 * Pure: fixed idt/idts vs. pttrn/pttrns syntactic categories; |
74 |
73 |
75 |
74 |
76 *** HOL *** |
75 *** HOL *** |
|
76 |
|
77 * HOL/simplifier: added infix function `addsplits': |
|
78 instead of `<simpset> setloop (split_tac <thms>)' |
|
79 you can simply write `<simpset> adsplits <thms>' |
77 |
80 |
78 * HOL/simplifier: terms of the form |
81 * HOL/simplifier: terms of the form |
79 `? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)' (or t=x) |
82 `? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)' (or t=x) |
80 are rewritten to |
83 are rewritten to |
81 `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t)' |
84 `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t)' |