Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] AExp.thy

view this post on Zulip Email Gateway (Aug 19 2022 at 16:30):

From: mahmoud abdelazim <m.abdelazim@icloud.com>
The following Lines is taken from AExp.thy
FullSizeRender.jpg

view this post on Zulip Email Gateway (Aug 19 2022 at 16:31):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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
signature.asc

Last updated: Apr 24 2024 at 20:16 UTC