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.
»~~/src/HOL/Library/Binomial.thy«.

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.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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