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
630 stars 142 forks source link

Local theorems don't show up in search results #1350

Open myreen opened 5 days ago

myreen commented 5 days ago 
Theorem foo[local]:
  1 + 2 + 3 = 6:num
Proof
  fs []
QED

(* the following don't print anything *)
print_match [] “_ = 6:num”;
print_find "foo";