[isabelle-dev] Some experiences with MicroJava, Jinja, JinjaThreads

[Tobias Nipkow]

> 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