search

RobArthan / pp

ProofPower is an open source suite of tools for specification and proof in HOL and Z.
http://www.lemma-one.com/ProofPower/index/index.html
Other
7 stars 3 forks source link

z_%exists%_intro and z_%exists%_elim #2

Open rbjones opened 8 years ago

rbjones commented 8 years ago

Though rules for introduction and elimination of universal quantifiers specific to z exist, the corresponding ones for existential quantifiers don't exist.

RobArthan commented 4 years ago

I'll have a look into this. It might be a good test case for transferring fixes and enhancements from pp to pp-utf8 (or pp2020, should I say?).