[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Question on operator

> I would like to know if another operator exists or if it is possible to
> define a new operator having the following behavior. I call op the
> operator.

> if we want to prove the sequent

> A op B
> C
> ---
> D

> I should prove the sequents

> --
> A

> and

> B
> C
> --
> D

   If you let op be => and use Hide -1 2 on the first subgoal after
   you issue prop you  get what you want.

Rick Butler  

   P.S. If you really are free to pick the "op" in a premise, the following
        might be very productive one:

           op(a,b: T): bool = FALSE