> The three obfuscating issues were: > > A) Archaic, hardly readable and fragile proof techniques: > * unfolding definitions of predicates over logical formulae instead of > proper intro/elim-rules
This is mere dogma. It is perfectly standard to reason about logical concepts by unfolding their definitions. If this is considered "archaic", we should force all Isabelle users to take vows to serve the church of natural deduction and renounce all other means of proof as heresy. Your other points are quite valid. Tobias
