]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 22f6a8f) | patch
Proof explosion improved (= avoided) for:
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 29 Aug 2001 15:16:25 +0000 (15:16 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 29 Aug 2001 15:16:25 +0000 (15:16 +0000)
commita0da07547d92d5bcb9f9eac2399ccb6b700b9d03
treec094962bfb0a3db8434ca2a902337f147c5fccf5tree | snapshot
parent22f6a8f49ed4015bf3c36f0036041932711248decommit | diff
Proof explosion improved (= avoided) for:
 1) Proofs after lambda-introductions (linear proofs)
 2) Proofs after a rewriting step (linear proofs)
 3) Proofs after a letin1 (linear proofs)
helm/style/mmlextension.xsl diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.