Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Printing inductive rules as proof trees

view this post on Zulip Email Gateway (Aug 22 2022 at 11:08):

From: Diego Machado Dias <diegodias.m@gmail.com>
In Chapter 7 of Concrete Semantics [1], the figures 7.1 and 7.2
show the same inductive predicate. The first (7.1) presents
each rule as a proof tree, while the second (7.2) shows the
inductive predicate as it is encoded in Isabelle.

It is said in the text that Figure 1 is generated automatically
with the help of Isabelle's LATEX pretty-printing facility.
Is there any document/example where I can see how this is
done? I searched on the tutorial and reference documents, but
I failed to find any hints about it.

Many thanks,

Regards,
Diego

  1. Concrete Semantics with Isabelle/HOL. Tobias Nipkow and Gerwin Klein.

view this post on Zulip Email Gateway (Aug 22 2022 at 11:08):

From: Alfio Martini <alfio.martini@acm.org>
Hi Diego,

I think here you will find what you need.

http://isabelle.in.tum.de/dist/Isabelle2015/doc/sugar.pdf

Best!

Last updated: Apr 18 2024 at 01:05 UTC