isabelle-prover / proving-contest-backends

"proving-contest"-backends for several theorem provers
MIT License
12 stars 5 forks source link

[Isabelle2020] Incomprehensible Error Message #29

Open wimmers opened 4 years ago

wimmers commented 4 years ago

If one uses imports Main instead of import Defs one gets the following incomprehensible error message: Internal error | writing theory files failed - (list index out of range) We should improve on this, as new users will likely run into that error very often.