]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ecdf96b) | patch
"obtain H E1=E2 by proof" is now working
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 21 Aug 2007 09:48:14 +0000 (09:48 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 21 Aug 2007 09:48:14 +0000 (09:48 +0000)
commitc84403b0c5272eb44adafa48ffaf6abdc637fc65
tree5892a4053df1b81c32dff2c3b61f23c84d8096e9tree | snapshot
parentecdf96be61f7f9cee7336b81d24780e59d1ea554commit | diff
"obtain H E1=E2 by proof" is now working
components/tactics/declarative.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.