Poscat (Oct 04 2026 at 10:51): Poscat (Oct 04 2026 at 10:51):I'm trying to build MK set/class theory on top of FOL and Is trying to define syntatic sugar for {t | x, y... . P} := {a | Exist x, y... . P /\ a = t} (for arbitrary term t). I looked up the source code HOL/HOL/Set.thy and found out that this is done using parse_translation and print_translation. Unfortunately I have no idea what the ML code in these commands mean nor how to adapt them to my use case. Is this documented somewhere?
Kevin Kappelmann (Oct 04 2026 at 11:22):The documentation for them is here https://isabelle.in.tum.de/doc/isar-ref.pdf
Given that there is a working example that you want to slightly adapt, you could also ask an AI agent to help you doing it (if you have access to one).
Poscat (Oct 04 2026 at 13:54):Codex did it with ease, I'm flabbergasted...
Last updated: Oct 19 2026 at 03:46 UTC