]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 013e0ab) | patch
procedural: added fwd rewrite in arbitrary proofs (not just premises)
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 12 Jan 2007 19:34:58 +0000 (19:34 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 12 Jan 2007 19:34:58 +0000 (19:34 +0000)
commit664ce15981e66bc897f31963b2f9f2f1e3d11470
tree4ed91449e06f5ac4ee4b3fd43d39c611860f4c52tree | snapshot
parent013e0ab5c86d7c4c7560f06ffe0ae3b424737db2commit | diff
procedural: added fwd rewrite in arbitrary proofs (not just premises)
            added whd conversion before intros when needed
prova.ma  : highlighted a bug with the "in" clause of the "match" constr.
helm/software/components/content_pres/.depend diff | blob | history
helm/software/components/content_pres/.depend.opt diff | blob | history
helm/software/components/content_pres/Makefile diff | blob | history
helm/software/components/content_pres/acic2Procedural.ml diff | blob | history
helm/software/components/content_pres/proceduralConversion.ml [new file with mode: 0644] blob
helm/software/components/content_pres/proceduralConversion.mli [new file with mode: 0644] blob
helm/software/components/content_pres/proceduralTypes.ml diff | blob | history
helm/software/components/content_pres/proceduralTypes.mli diff | blob | history
helm/software/matita/contribs/prova.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.