search

martinberger / hol-c

A proof-of-concept LCF-style interactive theorem prover for HOL(C)
Other
4 stars 1 forks source link

Replacing open Thm with opaque Thm #2

Closed martinberger closed 1 year ago

martinberger commented 1 year ago

The original code was a bit sloppy about the Thm class, in the sense that you could construct instances of Thm without using the logical rules. The new version is as Milner intended: only the logical rules let you create Thm instances.