[isabelle] Abbreviate propositions?
Is there syntax to abbreviate or define propositions? E.g. I can
Foo :: "sometype => bool
"Foo f == \<forall> X Y. ... --> ..."
but I would rather write something about the metalogic like:
Foo :: "sometype => prop
"Foo f == ... ==> ..."
Hopefully the leading universal quantifiers are implicit, and
meta-implication can be used in the body.
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
This archive was generated by a fusion of
Pipermail (Mailman edition) and