JacquesCarette / hol-light-qe

The HOL Light theorem prover (moved from Google code)
Other
7 stars 1 forks source link

Hole LEM PR #31

Closed sjjs7 closed 4 years ago

sjjs7 commented 4 years ago

Final PR with all current changes. Fixed up indenting on a number of files as well (will be more mindful of that- sorry!).

JacquesCarette commented 4 years ago

Otherwise, everything here seemed fine to me. But there are definitely some 'deep' QE things going on here that @wmfarmer needs to check in detail.

sjjs7 commented 4 years ago

@wmfarmer we've gone through most of these changes, but take a final look.

sjjs7 commented 4 years ago

This is good to commit.