Email Gateway (Aug 19 2022 at 16:30): 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
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: Nov 21 2024 at 12:39 UTC