NEWS
changeset 18044 f27022e2ec3a
parent 18020 d23a846598d2
child 18051 dba086ed50cb
equal deleted inserted replaced
18043:2427edb2e8a2 18044:f27022e2ec3a
    51 provided that "A" and "A ==> B" and "!!x. P x ==> Q x" are known
    51 provided that "A" and "A ==> B" and "!!x. P x ==> Q x" are known
    52 theorems in the current context, then these are valid literal facts:
    52 theorems in the current context, then these are valid literal facts:
    53 `A` and `A ==> B` and `!!x. P x ==> Q x" as well as `P a ==> Q a` etc.
    53 `A` and `A ==> B` and `!!x. P x ==> Q x" as well as `P a ==> Q a` etc.
    54 
    54 
    55 There is also a proof method "fact" which does the same composition
    55 There is also a proof method "fact" which does the same composition
    56 for explicit goals states, e.g. the following proof texts coincide
    56 for explicit goal states, e.g. the following proof texts coincide with
    57 with certain special cases of literal facts:
    57 certain special cases of literal facts:
    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`