]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f17163e) | patch
Notation for "ex" introduced. It is the same as the notation for forall,
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 19 Sep 2005 16:02:07 +0000 (16:02 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 19 Sep 2005 16:02:07 +0000 (16:02 +0000)
commit7efb15b93cf42eae8b34a12a327ee7213c1dbecc
tree47626a6eba5a4d177e87707b1b37b89dd1a0b1bdtree | snapshot
parentf17163e4895bdd6677da1616aafac0e5ee58c7d3commit | diff
Notation for "ex" introduced. It is the same as the notation for forall,
but it uses \exists.

NOTE: there is a bug now in cic_notation. The notation for ex is parsed, but
it is not pretty-printed correctly!
helm/matita/library/higher_order_defs/functions.ma diff | blob | history
helm/matita/library/logic/connectives.ma diff | blob | history
helm/matita/library/nat/factorization.ma diff | blob | history
helm/matita/library/nat/gcd.ma diff | blob | history
helm/matita/library/nat/minimization.ma diff | blob | history
helm/matita/library/nat/nth_prime.ma diff | blob | history
helm/matita/library/nat/orders.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.