Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] Manually using a SideKick parser

view this post on Zulip Email Gateway (Nov 17 2020 at 21:02):

From: MACKENZIE Carlin <s1724780@sms.ed.ac.uk>
Dear all,

I would like to run a parser, say "isabelle-context", from isabelle_sidekick.scala on a theory file and examine the output. Could someone advise on how to do this? I'm not sure where to look for an example call in the code

Thank you,
Carlin MacKenzie
The University of Edinburgh
The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.

view this post on Zulip Email Gateway (Nov 18 2020 at 07:00):

From: Makarius <makarius@sketis.net>
How is this related to the Isabelle development process?

You should ask this on the isabelle-users mailing list.

Makarius

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

view this post on Zulip Email Gateway (Nov 18 2020 at 12:26):

From: MACKENZIE Carlin <s1724780@sms.ed.ac.uk>
Sorry!

Carlin MacKenzie

Last updated: Apr 19 2024 at 12:27 UTC