anchor.diff:  
   //* ind_defs Module *//
   EXISTS_EQUATION;; // forces ind_defs module evaluation
  +!the_implicit_types;;                                                               // no change
  +type_abbrevs();;                                                                    // no change
   // No Changes in internal databases status: to be checked better
   
   // Class Module *//
  
positive.code: //   |- (==>) = (\p q. p /\ q <=> p);
  //   |- (/\) = (\p q. (\f. f p q) = (\f. f T T)); |- T <=> (\p. p) = (\p. p)]
  
  
  //* Num Module *//
  
  ONE_ONE;; // forces num module evaluation
negative.code: //   |- (==>) = (\p q. p /\ q <=> p);
  //   |- (/\) = (\p q. (\f. f p q) = (\f. f T T)); |- T <=> (\p. p) = (\p. p)]
  
  //ocaml
  
  //[|- one = (@x. T); |- I = (\x. x); |- (o) = (\f g x. f (g x));
  //   |- COND = (\t t1 t2. @x. ((t <=> T) ==> x = t1) /\ ((t <=> F) ==> x = t2));
  //   |- _FALSITY_ <=> F; |- (?!) = (\P. (?) P /\ (!x y. P x /\ P y ==> x = y));
  //   |- (~) = (\p. p ==> F); |- F <=> (!p. p);
  //   |- (\/) = (\p q. !r. (p ==> r) ==> (q ==> r) ==> r);
  //   |- (?) = (\P. !q. (!x. P x ==> q) ==> q); |- (!) = (\P. P = (\x. T));
  //   |- (==>) = (\p q. p /\ q <=> p);
  //   |- (/\) = (\p q. (\f. f p q) = (\f. f T T)); |- T <=> (\p. p) = (\p. p)]
  
  !the_implicit_types;;                                                               // internal database the_implicit_types
  //val it : (string * hol_type) list = []
  
  type_abbrevs();;                                                                    // internal database the_type_abbreviations
  //val it : (string * hol_type) list = []
  
  //monotonicity_theorems;;       only in ind_defs
  //{contents =
  //    [|- (A ==> B) /\ (C ==> D) ==> (if b then A else C) ==> (if b then B else D);
  //     |- (A ==> B) /\ (C ==> D) ==> A /\ C ==> B /\ D;
  //     |- (A ==> B) /\ (C ==> D) ==> A \/ C ==> B \/ D;
  //     |- (B ==> A) /\ (C ==> D) ==> (A ==> C) ==> B ==> D;
  //     |- (B ==> A) ==> ~A ==> ~B;
  //     |- (!x. P x ==> Q x) ==> (?x. P x) ==> (?x. Q x);
  //     |- (!x. P x ==> Q x) ==> (!x. P x) ==> (!x. Q x)];}
  
  // ocaml
  
  //{contents =
  //    [|- (A ==> B) /\ (C ==> D)
  //        ==> (if b then A else C)
  //        ==> (if b then B else D);
  //     |- (A ==> B) /\ (C ==> D) ==> A /\ C ==> B /\ D;
  //     |- (A ==> B) /\ (C ==> D) ==> A \/ C ==> B \/ D;
  //     |- (B ==> A) /\ (C ==> D) ==> (A ==> C) ==> B ==> D;
  //     |- (B ==> A) ==> ~A ==> ~B;
  //     |- (!x. P x ==> Q x) ==> (?x. P x) ==> (?x. Q x);
  //     |- (!x. P x ==> Q x) ==> (!x. P x) ==> (!x. Q x)]}
  
  
  //the_inductive_definitions;;   only in ind_defs
  
  //inductive_type_store;;        only after class
  //{contents =
  //    [("1", (1, |- !P. P one ==> (!x. P x), |- !e. ?fn. fn one = e));
  //     ("bool",
  //      (2, |- !P. P F /\ P T ==> (!x. P x), |- !a b. ?f. f F = a /\ f T = b))];}
  
  // ocaml 
  
  //val it : (string * (int * thm * thm)) list ref =
  //  {contents =
  //    [("1", (1, |- !P. P one ==> (!x. P x), |- !e. ?fn. fn one = e));
  //     ("bool",
  //      (2, |- !P. P F /\ P T ==> (!x. P x), |- !a b. ?f. f F = a /\ f T = b))]}
  
  //* Canon Module *//
  CONJ_ACI_RULE;; // forces canon module evaluation
  