Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Define a fun

Email Gateway (Aug 19 2022 at 16:30):

From: mahmoud abdelazim <m.abdelazim@icloud.com>
Hi
How to define a fun like fun_upd in Isabelle?
thanks

Email Gateway (Aug 19 2022 at 16:30):

From: Buday Gergely <gbuday@karolyrobert.hu>
Dear Mahmoud,

could you please specify what your fun_upd would do?

• Gergely

Email Gateway (Aug 19 2022 at 16:30):

From: Peter Lammich <lammich@in.tum.de>
You may look at how it is actually done in Isabelle:
In isabelle/jedit, type term "fun_upd", and goto its definition by
Ctrl+Click on "fun_upd".

Last updated: Nov 21 2024 at 12:39 UTC