[isabelle] programmatically adding a class relation



The following code

  val thy = let
    val subrel_t =
        Logic.mk_classrel (nclass,
                           "ArraysMemInstance.fourthousand_count")
    val subrel_th =
        Goal.prove_raw [] (cterm_of thy subrel_t) (tac thy [])
  in
    AxClass.add_classrel subrel_th thy before
    writeln("Proved " ^ nclass ^ " < fourthousand_count")
  end

produces the following error:

Exception-
   THM
      ("add_classrel: malformed class relation",
         0,
         ["OFCLASS('a, fourthousand_count_class)"]) raised

The theorem is proved, but then add_classrel complains.  What should I
do differently?

Michael.






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.