anchor.diff:  (* Set up interface map.                                                     *)
   (* ------------------------------------------------------------------------- *)
   
  -do_list (ignore << overload_interface) 
  +do_list (ExtCore.Choice.bindOrRaise << overload_interface) 
                              ["+", (parse_term @"int_add:int->int->int")
                               "-", (parse_term @"int_sub:int->int->int")
                               "*", (parse_term @"int_mul:int->int->int")
  
positive.code: (* Now define similar notions over the natural numbers.                      *)
  (* ------------------------------------------------------------------------- *)
  
  overload_interface("divides", (parse_term @"num_divides:num->num->bool")) |> ignore
  overload_interface("mod", (parse_term @"num_mod:num->num->num->bool")) |> ignore
  overload_interface("coprime", (parse_term @"num_coprime:num#num->bool")) |> ignore
  overload_interface("gcd", (parse_term @"num_gcd:num#num->num")) |> ignore
  
  let num_divides = new_definition(parse_term @"a divides b <=> &a divides &b")
  
  let num_mod = new_definition(parse_term @"(mod n) x y <=> (mod &n) (&x) (&y)")
  let num_congruent = 
      prove
          ((parse_term @"!x y n. (x == y) (mod n) <=> (&x == &y) (mod &n)"), 
           REWRITE_TAC [cong; num_mod])
  let num_coprime = new_definition(parse_term @"coprime(a,b) <=> coprime(&a,&b)")
  let num_gcd = new_definition(parse_term @"gcd(a,b) = num_of_int(gcd(&a,&b))")
  
  
negative.code:     let REW_RULE = GEN_REWRITE_RULE DEPTH_CONV thlist
  
      let int_tm_of_real_var v = 
          choice {
              let! s, ty = dest_var v
              if ty = real_ty then 
                  return! mk_comb(dest, mk_var(s, int_ty))
              else 
                  return v
          }
      
      let int_of_real_var v = 
          choice {
              let! s, ty = dest_var v
              if ty = real_ty then 
                  return mk_var(s, int_ty)
              else 
                  return v
          }
      
      let INT_OF_REAL_THM1 th = 
          choice {
              let! th = th
              let newavs = subtract (frees(concl th)) (freesl(hyp th))
              let avs, bod = strip_forall(concl th)
              let allavs = newavs @ avs
              let! avs' = Choice.List.map int_tm_of_real_var allavs
              let! avs'' = Choice.List.map int_of_real_var avs
              return! GENL avs'' (REW_RULE(SPECL avs' (GENL newavs (Choice.result th))))
          }
      
      let rec INT_OF_REAL_THM th = 
  