delete_binding
Theory.delete_binding : string -> unit
Remove a stored value from the current theory segment.
An invocation delete_binding s attempts to locate an axiom,
definition, or theorem that has been stored under name s in the
current theory segment. If such a binding can be found, it is deleted.
Failure
Never fails. If the binding can't be found, then nothing is removed from the current theory segment.
Example
> Define `fact x = if x=0 then 1 else x * fact (x-1)`;
val it = ⊢ ∀x. fact x = if x = 0 then 1 else x * fact (x − 1): thm
> current_theorems();
val it =
[("fact_ind", ⊢ ∀P. (∀x. (x ≠ 0 ⇒ P (x − 1)) ⇒ P x) ⇒ ∀v. P v),
("fact_def", ⊢ ∀x. fact x = if x = 0 then 1 else x * fact (x − 1))]:
(string * thm) list
> delete_binding "fact_ind";
val it = (): unit
> current_theorems();
val it =
[("fact_def", ⊢ ∀x. fact x = if x = 0 then 1 else x * fact (x − 1))]:
(string * thm) list
Comments
Removing a definition binding does not remove the constant(s) it
introduced from the signature. Use delete_const for that.
Removing an axiom has the consequence that all theorems proved from it become garbage.