Documentation update from HOL4: GEN_REWRITE_TAC

CJex / hol-light

HOL Light is an interactive theorem prover / proof checker. Automatically exported from code.google.com/p/hol-light

Other

1 stars 0 forks source link

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago

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 piotr.tr...@gmail.com on 7 Sep 2014 at 10:26

Attachments:

GoogleCodeExporter commented 9 years ago

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 jrh...@gmail.com on 16 Nov 2014 at 8:35