anchor.diff:  
   let (print_goal:goal->unit) =
     let string_of_int3 n =
  -    if n < 10 then "  "^string_of_int n
  -    else if n < 100 then " "^string_of_int n
  +    if n < 10 then "  " + string_of_int n
  +    else if n < 100 then " " + string_of_int n
       else string_of_int n in
     let print_hyp n (s,th) =
  -    open_hbox();
  +    Format.open_hbox();
       Format.print_string(string_of_int3 n);
       Format.print_string " [";
  -    open_hvbox 0;
  +    Format.open_hvbox 0;
       print_qterm (concl th);
  -    close_box();
  +    Format.close_box();
       Format.print_string "]";
  -    (if not (s = "") then (Format.print_string (" ("^s^")")) else ());
  -    close_box();
  +    (if not (s = "") then (Format.print_string (" (" + s + ")")) else ());
  +    Format.close_box();
       Format.print_newline() in
     let rec print_hyps n asl =
       if asl = [] then () else
  
positive.code: (* Install the goal-related printers.                                        *)
  (* ------------------------------------------------------------------------- *)
  
  #install_printer print_goal;;
  #install_printer print_goalstack;;
  
  *)
  
negative.code: let (USE_THEN:string->thm_tactic->tactic) =
    fun s ttac (asl,w as gl) ->
      let th = try assoc s asl with Failure _ ->
               failwith("USE_TAC: didn't find assumption " + s) in
      ttac th gl;;
  
  let (REMOVE_THEN:string->thm_tactic->tactic) =
    fun s ttac (asl,w) ->
      let th = try assoc s asl with Failure _ ->
               failwith("USE_TAC: didn't find assumption " + s) in
      let asl1,asl2 = chop_list(index s (map fst asl)) asl in
      let asl' = asl1 @ tl asl2 in
      ttac th (asl',w);;
  