[isabelle] Two questions of a beginner
I have two (plus one) questions:
1. blast, auto, ... are all GREAT!
But is there a way (in ProofGeneral) to see the proofs found by these
tools more detail?
2. If I have a non-atomic premise like:
[| A ==> B ; ... |] ==> C
how can I "use" it as a rule?
I am looking for somethink like:
apply (rule premise1)
3. Where could I have found answers to these questions?
This archive was generated by a fusion of
Pipermail (Mailman edition) and