- Explicitely applied predicate1I in a few proofs, because it is no longer
part of the claset
- Explicitely passed pred_subset_eq and pred_equals_eq as an argument to the
to_set attribute, because it is no longer applied automatically
Ref System Logics HOL ZF Inductive AxClass TutorialI IsarOverview IsarRef IsarImplementation Locales LaTeXsugar IsarAdvanced/Classes IsarAdvanced/Codegen IsarAdvanced/Functions