forked from Isabelle_DOF/Isabelle_DOF
2b1a9d009e
Support invariants on attributes of classes atttributes. Example: doc_class inv_test1 = a :: int doc_class inv_test2 = b :: "inv_test1" c:: int invariant inv_test2 :: "c σ = 1" invariant inv_test2' :: "a (b σ) = 2" doc_class inv_test3 = inv_test1 + b :: "inv_test1" c:: int invariant inv_test3 :: "a σ = 1" invariant inv_test3' :: "a (b σ) = 2" To support invariant on attributes in attributes and invariant on attributes of the superclasses, we check that the type of the attribute of the subclass is ground:› ML‹ val Type(st, [ty]) = \<^typ>‹inv_test1› val Type(st', [ty']) = \<^typ>‹'a inv_test1_scheme› val t = ty = \<^typ>‹unit› › |
||
|---|---|---|
| .. | ||
| figures | ||
| AssnsLemmaThmEtc.thy | ||
| Attributes.thy | ||
| Cenelec_Test.thy | ||
| Concept_Example.thy | ||
| Concept_Example_Low_Level_Invariant.thy | ||
| Evaluation.thy | ||
| High_Level_Syntax_Invariants.thy | ||
| Isabelle2022.thy | ||
| Ontology_Matching_Example.thy | ||
| OutOfOrderPresntn.thy | ||
| ROOT | ||
| TermAntiquotations.thy | ||