NEWS
changeset 20118 0c1ec587a5a8
parent 20090 5cf221f2a55d
child 20136 8e92a8f9720b
equal deleted inserted replaced
20117:0f7b7bfae82b 20118:0c1ec587a5a8
    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.: