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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
