Re: [isabelle] effect of declare in Isar



Jeremy Dawson wrote:

I understand from the Isabelle/Isar conversion guide that

declare zless2p zle2p [simp] ;

should add these theorems to the current simpset, just like
the ML function call

Addsimps [zless2p, zle2p] ;

No, the [simp] attribute in the above declaration is only applied to the
theorem occurring immediately before the attribute (i.e. zle2p), but not
to both zless2p and zle2p. If you want to achieve the same effect as the
above Addsimps command, you either have to write

  declare zless2p [simp] zle2p [simp]

or

  lemmas [simp] = zless2p zle2p

Greetings,
Stefan

--
Dr. Stefan Berghofer               E-Mail: berghofe at in.tum.de
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY            http://www.in.tum.de/~berghofe





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