*To*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] Qualified theory imports and isabelle jedit -l â -R â*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Thu, 24 Aug 2017 17:36:11 +0200*Organization*: TU Munich*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.2.1

Dear all, when inspecting a ÂbrokenÂ session (let as assume, HOL-Number_Theory), I used to invoke > isabelle jedit -l HOL-Number_Theory -R ../Number_Theory/Number_Theory.thy and everything worked out smoothly. With qualified theory imports emerged in future Isabelle2017, this is no longer the case: theory ÂResiduesÂ chokes on imports from HOL-Algebra. Inspecting the corresponding session entry in src/HOL/ROOT: > session "HOL-Number_Theory" (timing) in Number_Theory = "HOL-Computational_Algebra" + > â > sessions > "HOL-Algebra" > â it seems to be the case that -R operates on the direct ancestor session HOL-Computational_Algebra but not on the Âside pathÂ HOL-Algebra. Is that intended? I have the feeling that the current behaviour would diminish the usability of -R considerably. Cheers, Florian -- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

- Previous by Date: Re: [isabelle] Sequents: meaning of types o, seq', meaning of nonterminals seq, seqobj, seqcont
- Next by Date: [isabelle] Second CfP: MACIS 2017
- Previous by Thread: [isabelle] New AFP entry: Orbit-Stabiliser Theorem with Application to Rotational Symmetries
- Next by Thread: [isabelle] Second CfP: MACIS 2017
- Cl-isabelle-users August 2017 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list