anchor.diff:  //   ("F", bool); ("\/", bool->bool->bool); ("?", (A->bool)->bool);
   //   ("!", (A->bool)->bool); ("==>", bool->bool->bool); ("/\", bool->bool->bool);
   //   ("T", bool); ("=", A->A->bool)]
  -axioms();;                                                                          // new axioms: ETA, SELECT
  +axioms();;                                                                          // new axioms: SELECT, ETA
   //  [|- !P x. P x ==> P ((@) P); |- !t. (\x. t x) = t]
   definitions();;                                                                     // new COND definition
   //  [|- COND = (\t t1 t2. @x. ((t <=> T) ==> x = t1) /\ ((t <=> F) ==> x = t2));
  
positive.code: 
  *)
  
  #load "hol.fsx"
  
  //open NHol.lib
  //open NHol.fusion
  //open NHol.basics
  //open NHol.nets
  //open NHol.printer
  //open NHol.preterm
  //open NHol.parser
  //open NHol.equal
  //open NHol.bool
  //open NHol.drule
  //open NHol.tactics
  //open NHol.itab
  //open NHol.simp
  //open NHol.theorems
  //open NHol.ind_defs
  //open NHol.``class``
  //open NHol.trivia
  //open NHol.canon
  //open NHol.meson
  //open NHol.quot
  //open NHol.pair
  //open NHol.nums
  //open NHol.recursion
  //open NHol.arith   
  //open NHol.wf
  //open NHol.calc_num
  //open NHol.normalizer
  //open NHol.grobner
  
  //* Initial databases status *//
  
  
negative.code: //val it : (string * hol_type) list =
  //  [("=",
  //    Tyapp ("fun",[Tyvar "A"; Tyapp ("fun",[Tyvar "A"; Tyapp ("bool",[])])]))]
  
  infixes();;
  //val it : (string * (int * string)) list = []
  
  axioms();;                                                                          // internal database the_axioms
  //val it : thm list = []
  