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

Documentation update from HOL4: GEN_REWRITE_TAC #24

Open

GoogleCodeExporter opened this issue Oct 19, 2015 · 1 comment

Labels

auto-migrated Priority-Medium Type-Defect

GoogleCodeExporter commented Oct 19, 2015

Documentation for GEN_REWRITE_TAC seems to be copied from HOL4, but in HOL 
Light this tactic takes only two arguments, not three. Patch attached.

Original issue reported on code.google.com by [email protected] on 7 Sep 2014 at 10:26

Attachments:

GEN_REWRITE_TAC.diff

The text was updated successfully, but these errors were encountered:

Author

GoogleCodeExporter commented Oct 19, 2015

Actually this originates with the documentation for their common ancestor HOL88.
Thanks a lot for the patch, which I've finally applied in r205.

Original comment by [email protected] on 16 Nov 2014 at 8:35

GoogleCodeExporter added Priority-Medium Type-Defect auto-migrated labels

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