[isabelle] Renaming on code-export


in my theories I have a fun foo, but I'd like to have it called 'bar' in
my SML code (in usage and definition). Is this possible in general
(without having to add a function bar to Isabelle with the same content
as foo)?

I tried:

definition "bar = foo"
lemma [code_unfold]: "foo = bar" by (simp add: bar_def)

but this did not work out as expected.

René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

Attachment: smime.p7s
Description: S/MIME Kryptografische Unterschrift

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