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

Reinstate Reference Manual's list of theorems #41

Open
mn200 opened this issue Oct 14, 2011 · 1 comment
Open

Reinstate Reference Manual's list of theorems #41

mn200 opened this issue Oct 14, 2011 · 1 comment
Labels
Documentation Feature Request Low Priority

Comments

@mn200
Copy link
Member

mn200 commented Oct 14, 2011

The Reference manual used to include a big list of the core system's theorems. I found this useful when I was learning HOL, so perhaps we should try to do this again. It's not clear if we'd really want to list all theorems, even for just the core theories, but I guess a tool that included all theorems from specified theories except for ones that a developer somehow flagged as 'uninteresting' would be the way to go.

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.
@mn200 mn200 mentioned this issue Feb 18, 2014
Closed
mn200 added a commit that referenced this issue Feb 18, 2014
@mn200
Comment out paragraph in REFERENCE that claims two chapters.
4ae7ae9 
This can be put back once issue #41 is resolved.  Thanks to Rob
Arthan's comment in issue #151 for bringing this up.
mn200 added a commit that referenced this issue Sep 8, 2014
@mn200
Clean up pred_set/Manual a little.
2535a61 
Prompted by ptroja's commit in cd6153e.

Note that this material is desperately in need of a more comprehensive
update. The changes here are no more than a hint of how we might more
forward with this (there are similar remnants elsewhere).

In particular, the theorems in pred_set/help/thms should be generated,
and should probably be using EmitTeX technology rather than verbatim
rendering. See also github issue #41. The make process does not
correctly incorporate the manual style .doc entries, and those files
are probably wrong to boot.
@mn200
Copy link
Member Author

mn200 commented Apr 3, 2022

The flagging of theorems, whether white-listing (with associated categories?) or marking as interesting could obviously be done with theorem attributes.

mn200 added a commit that referenced this issue Apr 3, 2022
@mn200
Remove a variety of unused pretty-printed theorems
bfb7e2d 
See github issue #41 for more on this.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
Documentation Feature Request Low Priority
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@mn200