Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] class "Finite_Set.finite" now referred to by a...

Email Gateway (Aug 18 2022 at 11:13):

From: Michael Norrish <Michael.Norrish@nicta.com.au>
In some old code I had:

AxClass.prove_arity
(signm, [], ["Finite_Set.finite"])
(Class.intro_classes_tac [] THEN
asm_full_simp_tac (simpset_of thy addsimps
[eqn_th, @{thm "finite"}]) 1)
thy

This now fails with the error

*** exception TYPE raised: Undeclared class: "Finite_Set.finite"

This is despite the fact that there is still a class finite declared
in Finite_Set.thy. So, how should I refer to it? Or should I be
using something other than AxClass.prove_arity to do this job?

Michael.

Email Gateway (Aug 18 2022 at 11:13):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear Michael,

For technical reasons this class is currently named
"Finite_Set.finite.finite". Anyway you may use ML antiquotations to
make your code robust with respect to such naming issues:

AxClass.prove_arity
(signm, [], @{sort "Finite_Set.finite"}) ...

Hope this helps
Florian
florian.haftmann.vcf
signature.asc

Last updated: May 03 2024 at 04:19 UTC