equal
deleted
inserted
replaced
|
1 |
1 Isabelle NEWS -- history of user-visible changes |
2 Isabelle NEWS -- history of user-visible changes |
2 ================================================ |
3 ================================================ |
3 |
4 |
4 New in this Isabelle version |
5 New in this Isabelle version |
5 ---------------------------- |
6 ---------------------------- |
38 and ZF); |
39 and ZF); |
39 |
40 |
40 * new toplevel commands 'Thm' and 'Thms' for retrieving theorems from |
41 * new toplevel commands 'Thm' and 'Thms' for retrieving theorems from |
41 the current theory context; |
42 the current theory context; |
42 |
43 |
|
44 * new toplevel commands `Goal' and `Goalw' that improve upon `goal' |
|
45 and `goalw': the theory is no longer needed as an explicit argument - |
|
46 the current theory is used; assumptions are no longer returned at the |
|
47 ML-level unless one of them starts with ==> or !!; it is recommended |
|
48 to convert to these new commands using isatool fixgoal (as usual, |
|
49 backup your sources first!); |
|
50 |
43 * new theory section 'nonterminals'; |
51 * new theory section 'nonterminals'; |
44 |
52 |
45 * new theory section 'setup'; |
53 * new theory section 'setup'; |
46 |
54 |
47 |
55 |