]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 72dae1a) | patch
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)
commitd769719c7c60089f1623d7c31db992326b9408e2
tree96af69acb4d2559b33eb7513bb107a401fd25313tree | snapshot
parent72dae1a44bbed06ff9daeadf53671e109a1b882fcommit | diff
decompose: delta-expansion of the type to eliminate now works fine
components/tactics/eliminationTactics.ml diff | blob | history
matita/help/C/sec_tactics.xml diff | blob | history
matita/help/C/tactics_quickref.xml diff | blob | history
matita/tests/decompose.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.