equal
deleted
inserted
replaced
82 |
82 |
83 have "A" by fact == note `A` |
83 have "A" by fact == note `A` |
84 have "A ==> B" by fact == note `A ==> B` |
84 have "A ==> B" by fact == note `A ==> B` |
85 have "!!x. P x ==> Q x" by fact == note `!!x. P x ==> Q x` |
85 have "!!x. P x ==> Q x" by fact == note `!!x. P x ==> Q x` |
86 have "P a ==> Q a" by fact == note `P a ==> Q a` |
86 have "P a ==> Q a" by fact == note `P a ==> Q a` |
|
87 |
|
88 * Isar: ":" (colon) is no longer a symbolic identifier character in |
|
89 outer syntax. Thus symbolic identifiers may be used without |
|
90 additional white space in declarations like this: ``assume *: A''. |
87 |
91 |
88 * Isar: 'print_facts' prints all local facts of the current context, |
92 * Isar: 'print_facts' prints all local facts of the current context, |
89 both named and unnamed ones. |
93 both named and unnamed ones. |
90 |
94 |
91 * Isar: 'def' now admits simultaneous definitions, e.g.: |
95 * Isar: 'def' now admits simultaneous definitions, e.g.: |