[isabelle-dev] Fwd: Build of AFP entry Incompleteness failed
Lawrence Paulson
lp15 at cam.ac.uk
Thu Apr 6 20:30:38 CEST 2017
A very weird error has somehow appeared
Larry
> Begin forwarded message:
>
> From: Isabelle/Jenkins <ci at isabelle.systems>
> Subject: Build of AFP entry Incompleteness failed
> Date: 6 April 2017 at 18:02:58 BST
> To: lp15 at cam.ac.uk
>
> *** Failed to load theory "Nominal2_Abs" (unresolved "Nominal2_Base")
> *** Failed to load theory "Nominal2_FCB" (unresolved "Nominal2_Abs")
> *** Failed to load theory "Nominal2" (unresolved "Nominal2_Abs", "Nominal2_Base", "Nominal2_FCB")
> *** ML error (line 136 of "~~/afp/thys/Nominal2/nominal_eqvt.ML"):
> *** Value or constructor (the_inductive_global) has not been declared in structure Inductive
> *** At command "ML_file" (line 3437 of "~~/afp/thys/Nominal2/Nominal2_Base.thy")
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20170406/5e6542a4/attachment-0001.html>
More information about the isabelle-dev
mailing list