[isabelle-dev] Some experiences with MicroJava, Jinja, JinjaThreads
nipkow at in.tum.de
Mon Jul 28 11:50:00 CEST 2008
> 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.
More information about the isabelle-dev