anchor.diff:      withAxioms (model |> axioms |> Map.map (fun _ -> f)) model
   
   /// Maps a failing function f over the axioms of a model.
  -let tryMapAxioms (f : 'x -> Result<'y, 'e>) (model : Model<'x, 'dview>) : Result<Model<'y, 'dview>, 'e> =
  +let tryMapAxioms (f : 'x -> Result<'y, 'e>) (model : Model<'x, 'dview>)
  +    : Result<Model<'y, 'dview>, 'e> =
       lift (fun x -> withAxioms x model)
            (model
             |> axioms
  
positive.code:      *)
  
      /// A guarded item.
      /// The semantics of a Guarded Item is that the Item is to be taken as present
      /// in its parent context (eg a View) if, and only if, Cond holds.
      type Guarded<'a> = 
          { Cond : BoolExpr
            Item : 'a }
  
  
negative.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>
  