This repository has been archived on 2024-04-22. You can view files and clone it, but cannot push or open issues or pull requests.

Nicolas Méric 2b1a9d009e Add support invariants on attributes of attributes ... 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› ›		2023-01-13 08:27:26 +01:00
..
latex	Moved core ACM styles into DOF-core.sty.	2022-06-29 21:45:09 +01:00
Isa_COL.thy	More antiquotations	2022-12-02 13:50:16 +01:00
Isa_DOF.thy	Add support invariants on attributes of attributes	2023-01-13 08:27:26 +01:00
RegExpInterface.thy	More antiquotations from Isabelle2021-1/2022	2022-12-02 11:41:31 +01:00