I am experiencing a major breakdown of performance after updating my Isabelle system. I am using large records and locales, could this be the reason? Oddly, while it takes longer than expected to parse a record declaration, the real problem seems to be the statement of lemmas after it (not even their proofs?). In one theory, stuff that used to run through in about 5 seconds is now taking more than 30 minutes (and counting, I am stopping the process now). And stuff that used to run through in 12 minutes, now takes more than 3 hours (and counting, I am stopping that one also).
Is noone else experiencing problems like this?? Could it have something to do with the new type inference algorithms? Steven
