# [isabelle] Questions about . method

Just out of curiosity:
1) Why does the method assumption restrict the given facts to 0 or 1?

`2) Why does 'by this' seem to do the same thing? Example: Since I am
``using exclusively Isar for proves, I accustomed myself to state lemmas as
`
lemma
assumes "A" and "B" shows "C"
rather than as
lemma "A ==> B ==> C"
Now, e.g.,
lemma "A ==> B ==> A" .
lemma "A ==> B ==> A" by assumption
both works. When 'Isarfying' the lemma a bit more, like
lemma assumes "A" shows "B ==> A"
using assms .
lemma ssumes "A" shows "B ==> A"
using assms by assumption
it is still working. But with
lemma assumes "A" and "B" shows "A"

`it doesn't work any longer. Wouldn't it be nice, to have a short way of
``proving such simple statements (where one of the current facts solves
``the goal). E.g.,
`
lemma assumes "A" and "B" shows "A' using assms .

`And indeed, isn't that, what the documentation claims? In isar-ref.pdf
``on page 88, I read "this applies all of the current facts directly as
``rules."
`
cheers
chris

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*