]> matita.cs.unibo.it Git - helm.git/commit
decompose: delta-expansion of the type to eliminate now works fine
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 26 Feb 2007 13:36:43 +0000 (13:36 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 26 Feb 2007 13:36:43 +0000 (13:36 +0000)
commit1f974ca07c502d85c9a3760aaaf633bae3c84fb6
tree1c68c6fd918cced5b81d19e7bac5e4df552ea191
parent00e0c1d5cff8d5b5588185e1a70352a2e7a1a8e9
decompose: delta-expansion of the type to eliminate now works fine
helm/software/components/tactics/eliminationTactics.ml
helm/software/matita/help/C/sec_tactics.xml
helm/software/matita/help/C/tactics_quickref.xml
helm/software/matita/tests/decompose.ma