Hi, ich habe gerade Isabelle geupdatet auf meinem Rechner. Leider l?uft jetzt eine Theorie bei mir nicht mehr durch (und damit auch alles andere was ich so f?r meine t?gliche Arbeit brauche :-( )
Und zwar: Ich lade die Theorie mit 'use_thy "While"'. Nachdem ALLE lemmas in der Theorie erfolgreich abgearbeitet wurden, kommt eine exception: *** exception THM raised: Ill-typed instantiation Exception- TOPLEVEL_ERROR raised Es gibt keine ML-files, die noch geladen w?rden oder so. Im Proof-general kann ich die Theorie ohne Probleme durchlaufen lassen. Irgendwelche Ideen, was da schief laufen k?nnte? Steven
