Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] overriding "min" syntax/constant notation

view this post on Zulip Email Gateway (Aug 18 2022 at 13:08):

From: Lucas Dixon <ldixon@inf.ed.ac.uk>
I am wondering if it is possible to use the name "min", (and names of
other constants defined by Isabelle) for my own constant without
Isabelle writing my theory name in front of each occurrence...

theory GreatBigLongTheoryName
imports Main
begin

definition
min :: "'a => 'a => 'a"
where
...

from now on goals with "min" get printed GreatBigLongTheoryName.min

any suggestions?

cheers,
lucas

view this post on Zulip Email Gateway (Aug 18 2022 at 13:09):

From: Makarius <makarius@sketis.net>
You can globally disable the "unique_names" option of name spaces (either
in Proof General or directly via ML). An alternative is to tweak the
theory context via ``hide (open) min'' etc. in your theory.

Makarius

Last updated: May 03 2024 at 04:19 UTC