[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