[isabelle-dev] simp and ring_simps -- post release

Amine Chaieb chaieb at in.tum.de
Mon Nov 26 22:29:21 CET 2007

Previous message (by thread): [isabelle-dev] [Fwd: Re: [isabelle] Codegen from Hoare logics?]
Next message (by thread): [isabelle-dev] simp - ring_simps
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

It is very strange to me that

lemma "(x::int) - y = x + - y"
   apply simp

loops....

What happened?

Best,
Amine.

Previous message (by thread): [isabelle-dev] [Fwd: Re: [isabelle] Codegen from Hoare logics?]
Next message (by thread): [isabelle-dev] simp - ring_simps
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

More information about the isabelle-dev mailing list