dropped support for List.distinct in binding to SMT solvers: only few applications benefited from this support, and in some cases the smt method fails due to its support for List.distinct
Intro Ref System Logics HOL ZF Inductive TutorialI IsarOverview IsarRef IsarImplementation Locales LaTeXsugar Classes Codegen Functions Nitpick Main Sledgehammer