*To*: Omar Jasim <oajasim1 at sheffield.ac.uk>*Subject*: Re: [isabelle] Definition*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Thu, 31 Mar 2016 12:12:45 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CAAi=geumkTk+XnaTLj9kvN_MYEbiWnRQ4k6Ok-J-KyRgguEk0g@mail.gmail.com>*References*: <CAAi=geumkTk+XnaTLj9kvN_MYEbiWnRQ4k6Ok-J-KyRgguEk0g@mail.gmail.com>

> 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

**References**:**[isabelle] Definition***From:*Omar Jasim

- Previous by Date: [isabelle] Display of exceptions in Isabelle/jEdit
- Next by Date: Re: [isabelle] bash on Windows 10
- Previous by Thread: [isabelle] Definition
- Next by Thread: [isabelle] ADG 2016 2nd CFP - Automated Deduction in Geometry, Strasbourg, June, 27-29
- Cl-isabelle-users March 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list