Re: [isabelle] Definition



> On 30 Mar 2016, at 16:20, Omar Jasim <oajasim1 at sheffield.ac.uk> 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.