anchor.diff:  //   ("\/", bool->bool->bool); ("?", (A->bool)->bool); ("!", (A->bool)->bool);
   //   ("==>", bool->bool->bool); ("/\", bool->bool->bool); ("T", bool);
   //   ("=", A->A->bool)]
  +
  +// ocaml
  +
  +//[("PASSOC", `:((A#B)#C->D)->A#B#C->D`); ("UNCURRY", `:(A->B->C)->A#B->C`);
  +//   ("CURRY", `:(A#B->C)->A->B->C`); ("SND", `:A#B->B`); ("FST", `:A#B->A`);
  +//   (",", `:A->B->A#B`); ("REP_prod", `:A#B->A->B->bool`);
  +//   ("ABS_prod", `:(A->B->bool)->A#B`); ("mk_pair", `:A->B->A->B->bool`);
  +//   ("_FUNCTION", `:(?4069->?4073->bool)->?4069->?4073`);
  +//   ("_MATCH", `:?4047->(?4047->?4051->bool)->?4051`);
  +//   ("_GUARDED_PATTERN", `:bool->bool->bool->bool`);
  +//   ("_UNGUARDED_PATTERN", `:bool->bool->bool`);
  +//   ("_SEQPATTERN",
  +//    `:(?4005->?4002->bool)->(?4005->?4002->bool)->?4005->?4002->bool`);
  +//   ("GEQ", `:A->A->bool`); ("GABS", `:(A->bool)->A`); ("LET_END", `:A->A`);
  +//   ("LET", `:(A->B)->A->B`); ("one", `:1`); ("one_REP", `:1->bool`);
  +//   ("one_ABS", `:bool->1`); ("I", `:A->A`); ("o", `:(B->C)->(A->B)->A->C`);
  +//   ("COND", `:bool->A->A->A`); ("@", `:(A->bool)->A`);
  +//   ("_FALSITY_", `:bool`); ("?!", `:(A->bool)->bool`); ("~", `:bool->bool`);
  +//   ("F", `:bool`); ("\\/", `:bool->bool->bool`); ("?", `:(A->bool)->bool`);
  +//   ("!", `:(A->bool)->bool`); ("==>", `:bool->bool->bool`);
  +//   ("/\\", `:bool->bool->bool`); ("T", `:bool`); ("=", `:A->A->bool`)]
  +
   axioms();;                                                                          // no new axioms
   //  [|- !P x. P x ==> P ((@) P); |- !t. (\x. t x) = t]
  +
  +// ocaml
  +
  +//[|- !P x. P x ==> P ((@) P); |- !t. (\x. t x) = t]
  +
   definitions();;                                                                     // lots of new definitions
   //  [|- PASSOC =
   //   (\_1099 _1100. _1099 ((FST _1100,FST (SND _1100)),SND (SND _1100)));
  
positive.code: //   ("F", bool); ("\/", bool->bool->bool); ("?", (A->bool)->bool);
  //   ("!", (A->bool)->bool); ("==>", bool->bool->bool); ("/\", bool->bool->bool);
  //   ("T", bool); ("=", A->A->bool)]
  axioms();;                                                                          // the_axioms database doesn't change
  definitions();;                                                                     // new definitions one, I, (o)
  //  [|- 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));
  
negative.code: //   ("=", A->A->bool)]
  axioms();;                                                                          // the_axioms database doesn't change
  definitions();;                                                                     // the_definitions doesn't change
  !the_implicit_types;;                                                               // no change
  type_abbrevs();;                                                                    // no change
  
  // after population of constants this parses
  parse_term @"~(p /\ q) <=> ~p \/ ~q";;
  