[isabelle] Abbreviate propositions?



Is there syntax to abbreviate or define propositions?  E.g. I can
write:

  abbreviation
    Foo :: "sometype => bool
  where
    "Foo f == \<forall> X Y. ... --> ..."

but I would rather write something about the metalogic like:

  abbreviation
    Foo :: "sometype => prop
  where
    "Foo f == ... ==> ..."

Hopefully the leading universal quantifiers are implicit, and
meta-implication can be used in the body.

Thanks,
Randy

-- 
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 MHonArc.