[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 MHonArc.