anchor.diff:          | Failure _ -> ttac th g
       REPEAT_GTCL
   
  +/// Passes a theorem unchanged to a theorem-tactic.
   let (ALL_THEN : thm_tactical) = I
   
  +/// Theorem-tactical which always fails.
   let (NO_THEN : thm_tactical) = fun ttac th -> failwith "NO_THEN"
   
  +/// Composes a list of theorem-tacticals.
   let EVERY_TCL ttcll =
       itlist (fun t1 t2 -> t1 |> THEN_TCL <| t2) ttcll ALL_THEN;;
   
  +/// Applies the first theorem-tactical in a list that succeeds.
   let FIRST_TCL ttcll =
       end_itlist (fun t1 t2 -> t1 |> ORELSE_TCL <| t2) ttcll;;
   
  
positive.code:         SUBGOAL_THEN tm (LABEL_TAC s) |> THENL <| [p; ALL_TAC]
      |  [] -> failwith "SUBGOAL_TAC: no subproof given"
  
  let (FREEZE_THEN : thm_tactical) = 
      fun ttac th (asl, w) -> 
          let meta, gl, just = ttac (ASSUME(concl th)) (asl, w)
  
negative.code: (* A printer for goals etc.                                                  *)
  (* ------------------------------------------------------------------------- *)
  
  /// Print a goal to standard output, with no following newline.
  let (print_goal : goal -> unit) = 
      let string3 n = 
          if n < 10
  