scrub

Theory.scrub : unit -> unit

Remove all out-of-date elements from the current theory segment.

An invocation scrub() goes through the current theory segment and removes all out-of-date elements.

Failure

Never fails.

Example

In the following, we define a concrete type and examine the current theory segment to see what consequences of this definition have been stored there. Then we delete the type, which turns all those consequences into garbage. An query, like current_theorems, shows that this garbage is not collected automatically. A manual invocation of scrub is necessary to show the true state of play.

   - Hol_datatype `foo = A | B of 'a`;
   <<HOL message: Defined type: "foo">>
   > val it = () : unit

   - current_theorems();
   > val it =
       [("foo_induction", |- !P. P A /\ (!a. P (B a)) ==> !f. P f),
        ("foo_Axiom", |- !f0 f1. ?fn. (fn A = f0) /\ !a. fn (B a) = f1 a),
        ("foo_nchotomy", |- !f. (f = A) \/ ?a. f = B a),
        ("foo_case_cong",
         |- !M M' v f.
              (M = M') /\ ((M' = A) ==> (v = v')) /\
              (!a. (M' = B a) ==> (f a = f' a)) ==>
              (case v f M = case v' f' M')),
        ("foo_distinct", |- !a. ~(A = B a)),
        ("foo_11", |- !a a'. (B a = B a') = (a = a'))] : (string * thm) list

   - delete_type "foo";
   > val it = () : unit

   - current_theorems();
   > val it =
       [("foo_induction", |- !P. P A /\ (!a. P (B a)) ==> !f. P f),
        ("foo_Axiom", |- !f0 f1. ?fn. (fn A = f0) /\ !a. fn (B a) = f1 a),
        ("foo_nchotomy", |- !f. (f = A) \/ ?a. f = B a),
        ("foo_case_cong",
         |- !M M' v f.
              (M = M') /\ ((M' = A) ==> (v = v')) /\
              (!a. (M' = B a) ==> (f a = f' a)) ==>
              (case v f M = case v' f' M')),
        ("foo_distinct", |- !a. ~(A = B a)),
        ("foo_11", |- !a a'. (B a = B a') = (a = a'))] : (string * thm) list

   - scrub();
   > val it = () : unit

   - current_theorems();
   > val it = [] : (string * thm) list

When export_theory is called, it uses scrub to prepare the current segment for export. Users can also call scrub to find out what setting they are really working in.

See also

Theory.uptodate_type, Theory.uptodate_term, Theory.uptodate_thm, Theory.delete_type, Theory.delete_const