On 24/04/17 14:36, Makarius wrote:
> On 23/04/17 18:10, Blanchette, J.C. wrote:
>>
>> *** No such file:
>> "/Users/blanchette/isabelle/src/HOL/Library/Fraction_Field.thy"
>> *** The error(s) above occurred for theory "HOL-Lib.Fraction_Field" (line 17
>> of "/Users/blanchette/hgs/isafor/thys/ROOT")
>
> The transition from unqualified theories to qualified theories is not
> smooth -- there can be intermediate situations, where certain sessions
> cannot import certain theories anymore.
>
> The emerging tool "isabelle imports" tools helps to sort out the
> situation, but it requires some care to use it and I am still exploring
> the overall situation.
The situation is actually more basic: src/HOL/Library/Fraction_Field.thy
etc. were moved to a separate session in fc41a5650fb1 and thus you have
a broken IsaFoR still lying around by accident.
What I said about "isabelle imports" is not yet relevant (presently at
10f4a17e5928), because I did not move that far ahead yet -- although I
was pondering when to do it.
(Right now I have the impression that there is an aversion to any kind
of change on the ever changing isabelle-dev repository. We are between
the releases and now is the usual time for bigger reforms. Or are we
already in a state where big things can no longer happen?)
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
