[isabelle-dev] HOL-Predicate_Compile_Examples

Makarius makarius at sketis.net
Wed Sep 9 11:37:31 CEST 2015

Doing some routine maintenance, I've rediscovered this very odd changeset:

changeset:   40055:1f7cc5357d96
user:        bulwahn
date:        Thu Oct 21 20:26:35 2010 +0200
files:       src/HOL/Predicate_Compile_Examples/ROOT.ML
temporary removed Predicate_Compile_Quickcheck_Examples from tests

The comment in the source says "should be added again soon", but that was 
5 years ago.

The session HOL-Predicate_Compile_Examples has a few more dead and 
half-rotten bits, see 

Any ideas what can be done about it?  Even just removing rubbish requires 
some basic understanding of the situation.


More information about the isabelle-dev mailing list