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

Tobias Nipkow 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 mailing list