Re: [isabelle] Definition

> On 30 Mar 2016, at 16:20, Omar Jasim <oajasim1 at> wrote:
> lemma subset_u: "u â signal T R " unfolding signal_def by blast
> Its proved but I think there is problem with using blast as it highlight in
> purple!

There are some big misunderstandings here. Because u is a variable, proving subset_u would mean that signal T R was the universal set. 

> definition sos :: "_"
> where  "sos T R = {u | u. u â signal T R }â

This definition makes sos identical to signal, so probably you had something else in mind.

Larry Paulson

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