On 05/30/2011 06:03 PM, Lukas Bulwahn wrote:
On 05/30/2011 12:33 PM, Andreas Lochbihler wrote:
Hi Lukas,
here is an example that I would have expected to work. However,
congruences seem to work other than I expected. Du you know what I am
missing here?
theory Scratch imports Main begin
Hi Andreas,
the following ML line should do the job of adding the congruence rule in
your case:
setup {* Code_Preproc.map_pre (fn ss = ss addcongs [@{thm conj_cong}]) *}
Before we add yet another feature to the code generation setup in Isar,
we would like to understand your scenario.
Does
On 05/30/2011 12:33 PM, Andreas Lochbihler wrote:
Hi Lukas,
here is an example that I would have expected to work. However,
congruences seem to work other than I expected. Du you know what I am
missing here?
theory Scratch imports Main begin
definition test where test xs = (last xs = 0)
Does the current attribute mechanism support selective attributes such
as [code_inline cong], maybe along the lines of [simp del]? If it does,
I assume it would be easy to add that information in the place that
Florian pointed to?
Tobias
Am 28/05/2011 14:45, schrieb Florian Haftmann:
Hi
