In current 7ff7fdfbb9a0 there is this breakdown: HOL-Quickcheck_Examples FAILED *** No specification for Abs_filter *** At command "quickcheck" (line 150 of "~~/src/HOL/Quickcheck_Examples/Hotel_Example.thy") *** No specification for Abs_filter *** At command "quickcheck" (line 145 of "~~/src/HOL/Quickcheck_Examples/Hotel_Example.thy")
Since there is no way around a full "isabelle build -a" before pushing anything, such incidents can't happen, at least in theory.
Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev