anchor.diff:      let printSTerm pWPre pGoal = printTerm printBoolExpr pWPre pGoal
   
       /// Pretty-prints model variables.
  -    let printModelVar (name, ty) = 
  +    let printModelVar (name, ty) =
           colonSep [ String name
                      printType ty ]
   
  
positive.code:     let printViewDef pView { View = vs; Def = e } =
          printAssoc Inline
              [ (String "View", pView vs)
                (String "Def", withDefault (String "?") (Option.map printBoolExpr e)) ]
  
      /// Pretty-prints the axiom map for a model.
      let printModelAxioms pAxiom model =
          printMap Indented String pAxiom model.Axioms
  
      /// Pretty-prints a model given axiom and defining-view printers.
      let printModel pAxiom pDView model = 
          headed "Model" 
              [ headed "Shared variables" <|
                    Seq.singleton (printMap Inline String printType model.Globals)
                headed "Thread variables" <|
                    Seq.singleton (printMap Inline String printType model.Locals)
                headed "ViewDefs" <| List.map (printViewDef pDView) model.ViewDefs
                headed "Axioms" <| Seq.singleton (printModelAxioms pAxiom model) ]
      
      /// <summary>
      ///     Enumerations of ways to view part or all of a <c>Model</c>.
      /// </summary>
  
negative.code:      *)
  
      /// <summary>
      ///     A term, containing a command relation, weakest precondition, and
      ///     goal.
      /// </summary>
      /// <remarks>
      ///     Though these are similar to Axioms, we keep them separate for
      ///     reasons of semantics: Axioms are literal Hoare triples {P}C{Q},
      ///     whereas Terms are some form of the actual Views axiom soundness
      ///     check we intend to prove.
      /// </remarks>
      type Term<'cmd, 'wpre, 'goal> =
          { /// The command relation of the Term.
  