Quoting Lawrence Paulson <l...@cam.ac.uk>:
I got this message several times when converting theories. There is a workaround, but nevertheless, I think this is a bug.
Hi Larry, the reason for this problem is the removal of the rules pred_equals_eq and pred_subset_eq from the rule database used for the predicate / set conversion: http://isabelle.in.tum.de/repos/isabelle/rev/a6cb51c314f2 The conversion of lists_mono to predicate notation already failed before the re-introduction of the set type, but this did not cause an error message because the monotonicity rule for listsp was already part of the database of monotonicity rules, and the ill-formed monotonicity rule was simply ignored. Now that sets are no longer predicates, the conclusion of the ill-formed rule {x. ?A x} <= {x. ?B x} ==> {x. listsp ?A x} <= {x. listsp ?B x} is no longer an inequality between predicates, and so the rule is rejected. I will revert (parts of) the above changeset, and maybe also the related ones http://isabelle.in.tum.de/repos/isabelle/rev/0af0f674845d http://isabelle.in.tum.de/repos/isabelle/rev/a27607030a1c Do you still remember in which theories you applied your workaround? Maybe we should take a look at them again. Greetings, Stefan _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev