NEWS
 changeset 18044 f27022e2ec3a parent 18020 d23a846598d2 child 18051 dba086ed50cb
equal 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``