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

[Florian Haftmann]

Tobias Nipkow wrote:
>> 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.

Ignore the moody "archaic" but not the "fragile".  IMHO the problem
enters the stage iff such unfold series occur in larger apply scripts
because then these become more cluttered due to the need of breaking
down the object logic level connectives (stemming from the unfolded
definitions) to the meta logic connectives.

	Florian
-------------- next part --------------
A non-text attachment was scrubbed...
Name: florian.haftmann.vcf
Type: text/x-vcard
Size: 654 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20080728/dc943c22/attachment-0002.vcf>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 185 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20080728/dc943c22/attachment.sig>