Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Remove superseded lcsymtacs structure #666

Closed
mn200 opened this issue Feb 25, 2019 · 3 comments
Closed

Remove superseded lcsymtacs structure #666

mn200 opened this issue Feb 25, 2019 · 3 comments
Labels
Feature Request

Comments

@mn200
Copy link
Member

mn200 commented Feb 25, 2019

Given implementation of issues such as #274 and #275, the lcsymtacs module in src/boss seems unnecessary. (All it does by way of implementation is open a bunch of other modules.)
arolle added a commit to arolle/HOL that referenced this issue May 22, 2020
@arolle
remove lcsymtacs (github issue HOL-Theorem-Prover#666)
2807cf8 
The lcsymtacs structure is regarded superseded as it plainly is
a shorthand for opening the following modules:
Abbrev HolKernel boolLib Tactic Tactical BasicProvers simpLib
Rewrite bossLib Thm_cont
@arolle
Copy link
Contributor

arolle commented May 22, 2020

Before creating a pull request I have one question:
Are there any severe implications from simply removing an open lcsymtacs statement from a theory script in src (if it compiles without it), e.g. from src/new-datatype/NDDB.sml?

@mn200
Copy link
Member Author

mn200 commented May 24, 2020

No, there shouldn't be any issues with doing that. — Thanks!

mn200 pushed a commit that referenced this issue Jun 22, 2020
@arolle
remove lcsymtacs (github issue #666)
5417af9 
The lcsymtacs structure is regarded superseded as it plainly is
a shorthand for opening the following modules:
Abbrev HolKernel boolLib Tactic Tactical BasicProvers simpLib
Rewrite bossLib Thm_cont
@mn200
Copy link
Member Author

mn200 commented Jun 24, 2020

Closed by 5417af9

@mn200 mn200 closed this as completed Jun 24, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
Feature Request
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@mn200 @arolle