anchor.diff:      (* ----------------------------------------------------------------------- *)
       (* Try expansion and continuation call with ancestor or initial rule.      *)
       (* ----------------------------------------------------------------------- *)
  +
       let meson_expand rules ((g, ancestors), ((insts, offset, size) as tup)) cont = 
           let pr = fst g
           let newancestors = insertan insts g ancestors
  
positive.code: 
  open FSharp.Compatibility.OCaml
  open FSharp.Compatibility.OCaml.Num
  
  open NHol
  open lib
  
negative.code:                                                       (parse_term @"x:A = y")
                                                 |> THEN <| ASM_REWRITE_TAC []
                                                 |> THEN <| CONV_TAC TAUT)
  
          let imp_elim_CONV = REWR_CONV(TAUT(parse_term @"(a ==> b) <=> ~a \/ b"))
          let eq_elim_RULE = MATCH_MP(TAUT(parse_term @"(a <=> b) ==> b \/ ~a"))
          let veq_tm = Choice.get <| rator(Choice.get <| rator(concl <| Choice.get(hd eq_thms)))
  
          let create_equivalence_axioms(eq, _) = 
              let tyins = Choice.get <| type_match (Choice.get <| type_of veq_tm) (Choice.get <| type_of eq) []
              map (INST_TYPE tyins) eq_thms
  
          let rec tm_consts tm acc = 
              let fn, args = strip_comb tm
              if args = [] then acc
              else itlist tm_consts args (insert (fn, length args) acc)
  
          (* OPTIMIZE :   Modify the code below to use option instead of try/catch. *)
  