equal
deleted
inserted
replaced
58 |
58 |
59 have "A" by fact == note `A` |
59 have "A" by fact == note `A` |
60 have "A ==> B" by fact == note `A ==> B` |
60 have "A ==> B" by fact == note `A ==> B` |
61 have "!!x. P x ==> Q x" by fact == note `!!x. P x ==> Q x` |
61 have "!!x. P x ==> Q x" by fact == note `!!x. P x ==> Q x` |
62 have "P a ==> Q a" by fact == note `P a ==> Q a` |
62 have "P a ==> Q a" by fact == note `P a ==> Q a` |
|
63 |
|
64 * Isar: 'def' now admits simultaneous definitions, e.g.: |
|
65 |
|
66 def x == "t" and y == "u" |
63 |
67 |
64 * Provers/induct: improved internal context management to support |
68 * Provers/induct: improved internal context management to support |
65 local fixes and defines on-the-fly. Thus explicit meta-level |
69 local fixes and defines on-the-fly. Thus explicit meta-level |
66 connectives !! and ==> are rarely required anymore in inductive goals |
70 connectives !! and ==> are rarely required anymore in inductive goals |
67 (using object-logic connectives for this purpose has been long |
71 (using object-logic connectives for this purpose has been long |