On 10/10/17 20:50, Makarius wrote:
> The above change to AFP is required to avoid cyclic dependency of
> Jordan_Normal_Form vs. Polynomial_Factorization, due to session JNF-AFP-Lib.
>
> This problem can be exhibited as follows (without the change):
>
> Exn.capture {
On 10/10/17 20:50, Makarius wrote:
>
> import isabelle._
>
> val options = Options.init
> val afp = AFP.init(options)
>
> isabelle.graphview.Graph_File.write(options +
> "graphview_font_size=24", Path.explode("afp.pdf").file,
> afp.entries_graph_display)
>
> The resulting afp.pdf is
On 12/10/17 21:49, Makarius wrote:
> In Isabelle/c75769065548 I have refined the tool further to print
> "actual session dependencies", based on the imported theories and
> minimized according to the session imports relation.
The new "isabelle imports -I" also helps to determine logically
Here is some further simplification proposed by "isabelle imports -I".
One could probably also eliminate Sepref_Prereq. The maintainers of
these AFP entries need to say what is the purpose of that extra complexity.
(In the months before the Isabelle2017 release, I spent considerable
time to
