locale A = fixes foo :: "'a => 'b => nat" locale B = A1: A[where 'a = 'aa and 'b = 'bb] foo1 + A2: A[where 'a = 'cc and 'b = 'bb] foo2 for foo1 and foo2The alternative is to write type annotations on the constants in the
forclause, which gets very verbose for big locales.
locale A = fixes foo :: "'a => 'b => nat" locale B = namespace: A concretefoo + assumes somelemma: "... namespace.foo ... concretefoo ..."
datatype ('a, 'b, 'c) sometype = MkSomeType 'a 'b 'c context fixes foo :: "'a => 'b => 'c => bool" begin type_synonym mytype = "('a, 'b, 'c) sometype" end
-voption, print the verification time of the individual theories, and not just of the session.
-voption, the theories should be only displayed when their verification successfully completed, and not when it starts as is now the case.