force new theory
This procedure is for making a new theory in a context where a previous version of the same theory could be present and if so should be deleted (even if it has children).
xlsml
fun force_new_theory name =
let
val _ = force_delete_theory name handle _ => ();
in
new_theory name
end;


force new proof context
This procedure is for making a new pc in a context where a previous version of the pc could be present and if so should be deleted.
xlsml
fun force_new_pc name =
let
val _ = delete_pc name handle _ => ();
in
new_pc name
end;


Adding new theorems
The following procedure just abbreviates the process of adding one or more theorems for rewriting and for stripping.

Consistency Proofs
To permit hand consistency proofs to be completed before a HOLCONST specification we provide a consistency prover which just looks up a standard location for the consistency proof and put this in a proof context.
