[isabelle-dev] Bad state of repository

Makarius makarius at sketis.net
Tue Jul 1 22:33:34 CEST 2014


We have some unclear readings on 
http://isabelle.in.tum.de/reports/Isabelle and termination problems with 
HOL-Library.


One round of manual bisection yields the following, within the usual 
margin of error:

changeset:   57470:9512b867259c
user:        blanchet
date:        Tue Jul 01 16:49:25 2014 +0200
summary:     fixed soundness bug in monotonicity-based type encodings -- 
the helper facts must be considered too


In contrast, the point where Johannes applied some changes to HOL/Library 
seems to be OK: 2baecef3207f.


 	Makarius


More information about the isabelle-dev mailing list