Re: [isabelle] Two questions of a beginner



You can see some aspects of proofs using proof objects, but it's about as illuminating as reading the assembly language code produced by a compiler.

The answer to your second question is to use a structured proof. Non-atomic premises are all but useless in the apply style. In a structured proof, you can use such a thing exactly like an inference rule.

You will find plenty of Isabelle documentation here: http://isabelle.in.tum.de/documentation.html

Larry Paulson


On 18 Jan 2013, at 02:05, Not Sure <kuerzn at googlemail.com> wrote:

> 
> 
> Hi!
> 
> 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?
> 
> 
> Thanks!
> 
> 
> Johannes
> 
> 






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