Re: [isabelle] can't prove "True => True"



Thanks - this in conjuction with eval did the trick!

	Duraid

On Mon, Nov 10, 2008 at 05:31:35PM +0800, Tjark Weber wrote:
> On Mon, 2008-11-10 at 00:57 +0900, Duraid Madina wrote:
> > [...] I am not sure why, for example,
> > 
> > lemma doh:
> >  "1+1=(3::nat) --> 1+1=(4::nat)"
> > apply(eval)
> > done
> > 
> > works, but
> > 
> > lemma doh:
> >  "1+1=(3::nat) ==> 1+1=(4::nat)"
> > apply(eval)
> > done
> > 
> > fails. Is this exception the intended behaviour for the latter case?
> 
> I don't know if the above is the intended behavior, but in any case you 
> can replace the meta implication ==> by a HOL implication --> using
> 
>   apply (erule rev_mp)
> 
> More generally, you can replace meta connectives by HOL connectives
> using
> 
>   apply (atomize (full))
> 
> (See page 107 of the Isabelle/Isar Reference Manual for details.)
> 
> Best,
> 
>     Tjark
> 





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