diff options
| author | Son Ho | 2023-05-22 15:23:48 +0200 |
|---|---|---|
| committer | Son HO | 2023-06-04 21:54:38 +0200 |
| commit | 1f0e5b3cb80e9334b07bf4b074c01150f4abd49d (patch) | |
| tree | e66c708351b518bcda12bfa28ef3249eb3714cdb /backends/hol4/evalLib.sig | |
| parent | 77d775ecea850576b24d097b402571889faa2a15 (diff) | |
Make the unfolding theorems collection from evalLib persistent
Diffstat (limited to '')
| -rw-r--r-- | backends/hol4/evalLib.sig | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/backends/hol4/evalLib.sig b/backends/hol4/evalLib.sig index d045d3bb..f44cff13 100644 --- a/backends/hol4/evalLib.sig +++ b/backends/hol4/evalLib.sig @@ -8,10 +8,7 @@ sig include Abbrev - (* The following functions allow to register custom unfolding theorems *) - (* TODO: permanence of theorems? *) - val add_unfold : term * thm -> unit - val add_unfolds : (term * thm) list -> unit + (* The following functions allow to *persistently* register custom unfolding theorems *) val add_unfold_thm : thm -> unit val add_unfold_thms : thm list -> unit |