Re: [isabelle] assumptions format in isar



On Mon, 2 Oct 2006, Julien wrote:

> Then, I have a goal and a bunch of facts in "using this".
> 
> For technical reasons I need to have the same behavior as if I would type:
> main
> apply (insert foo1)
> apply (insert foo2)

Just do ``apply -'' here.


	Makarius





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