[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
description:
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 
http://isabelle.in.tum.de/repos/isabelle/file/f9fd43d8981d/src/HOL/ROOT#l973

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


 	Makarius



More information about the isabelle-dev mailing list