[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