A very weird error has somehow appeared Larry > Begin forwarded message: > > From: Isabelle/Jenkins <ci@isabelle.systems> > Subject: Build of AFP entry Incompleteness failed > Date: 6 April 2017 at 18:02:58 BST > To: l...@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") >
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
