Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] global_interpretation of residues fails

view this post on Zulip Email Gateway (Aug 23 2022 at 09:37):

From: Norbert Schirmer <cl-isabelle-users@lists.cam.ac.uk>
Dear all,

The following global interpretation fails (HOL-Number_Theory.Residues):

global_interpretation residues "int 3" "residue_ring 3"
apply unfold_locales
apply auto
done

(*
Duplicate fact declaration "Residues_Interpretation.cring" vs. "Residues_Interpretation.cring"⌂
The above error(s) occurred while activating facts of locale instance
residues "int 3" "residue_ring 3"
*)

Also find a potential patch with respect to revision 787a203a20b6.

Regards,
Norbert
Residues_Interpretation.thy
residues.patch
residues_regression.patch

view this post on Zulip Email Gateway (Aug 23 2022 at 15:47):

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

thanks for reporting this.

I will look after the patches.

Florian

Am 23.08.22 um 11:37 schrieb Norbert Schirmer (via cl-isabelle-users
Mailing List):
OpenPGP_signature

view this post on Zulip Email Gateway (Aug 25 2022 at 06:15):

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

done in https://isabelle.sketis.net/repos/isabelle/rev/884dbbc8e1b3

Cheers,
Florian
OpenPGP_signature

Last updated: Jan 04 2025 at 20:18 UTC