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://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20080728/dc943c22/attachment.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://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20080728/dc943c22/attachment.pgp