Skip to content

Add a bundle no_UTP_lattice_syntax to switch off UTP lattice syntax#8

Open
RandallYe wants to merge 1 commit intomainfrom
no_utp_lattice_syntax
Open

Add a bundle no_UTP_lattice_syntax to switch off UTP lattice syntax#8
RandallYe wants to merge 1 commit intomainfrom
no_utp_lattice_syntax

Conversation

@RandallYe
Copy link
Copy Markdown
Collaborator

In my mechanisation, I don't need lattice syntax from UTP and would use the lattice syntax from Isabelle HOL. For this reason, I have added a bundle no_UTP_lattice_syntax to switch off UTP lattice syntax.

By the way, I change the name utp_lattice_syntax to UTP_lattice_syntax to make its name consistent with other bundle names in UTP, like UTP_Logic_Syntax.

After this update, I have the following commands at the beginning of my theory:

unbundle UTP_Syntax
(* Switch off lattice syntax from UTP )
unbundle no_UTP_lattice_syntax
(
Switch on lattice syntax from HOL *)
unbundle lattice_syntax

@RandallYe
Copy link
Copy Markdown
Collaborator Author

@simondfoster do you think this change can be adopted by UTP? I think it might be useful in the future for other users. If not, I probably consider leaving this change locally in my theories. I need to make a decision about which way I will use it in my code because I need to hardcode the links to the theories in a paper.

Any questions, please do let me know. Thanks.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant