Automatic derivation of instances via DrIFT-rule ShATermConvertible for the type(s): AltSyntax VName QName Indexname IsaClass Typ Continuity TAttr DTyp Term Prop Props Sentence DefEquation FixrecEquation Ctxt Mixfix MixfixTemplate Datatype DatatypeConstructor Domain DomainConstructor DomainConstructorArg Axiom FunSig SetDecl MetaTerm TypeSig BaseSig Sign IsaProof ProofCommand ProofEnd Modifier ProofMethod