diff options
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 |