> * Antiquotation "lemma" takes a proposition and a simple method text as > argument > and asserts that the proposition is provable by the corresponding method > invocation. Prints text of proposition, as does antiquotation "prop". A > simple > method text is either a method name or a method name plus (optional) method > arguments in parentheses, mimicing the conventions known from Isar proof text. > Useful for illustration of presented theorems by particular examples.
-------------- 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/20080429/cabea975/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/20080429/cabea975/attachment.pgp
