search

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
https://hol-theorem-prover.org
Other
621 stars 140 forks source link

Add paragraph on Inductive definitions using modern syntax #1174

Closed rsoeldner closed 9 months ago

rsoeldner commented 9 months ago

This PR adds a small paragraph on the use of named rules in Inductive definitions.

image

mn200 commented 9 months ago

Thanks! Could add a sentence also explaining that the leading tilde is optional but is replaced by the stem (word after Inductive keyword) and an underscore?

rsoeldner commented 9 months ago

image

mn200 commented 9 months ago

Awesome! Many thanks.