Re: [isabelle] AExp.thy

Hi Machmud,

> The following Lines is taken from AExp.thy

just two hints: references to particular theories in the Isabelle
distribution are best given using explicit Isabelle paths, e.g.

This mail also shows why posting images without need is inconvenient:
they can get lost quite easily.  Under normal circumstances, it should
not be difficult to copy and paste Isar text from Isabelle/jEdit into a
mail client.

Concerning your concrete question: it's about fancy syntax.  You can
find hints in the Isabelle reference manual.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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