matita.cs.unibo.it Git - helm.git/commit

]> matita.cs.unibo.it Git - helm.git/commit

author	Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
	Wed, 1 Apr 2009 22:37:06 +0000 (22:37 +0000)
committer	Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
	Wed, 1 Apr 2009 22:37:06 +0000 (22:37 +0000)
commit	5fa31e43ffe25aa7b1539653b137968b5cf9899a
tree	45de09d7c7ea6bacde25e0e66cd1afe847899c87	tree \| snapshot
parent	dee331ab42d5d625f32fecc3e70df013c2dd093d	commit \| diff

New tactic "case1_tac" that make "intro" followed by case of the first
argument.

It is now possible to write things like:

napply t; ## [ #H | *W; #K1 #K2 ]

Unnamed repository; edit this file 'description' to name the repository.

RSS Atom

helm/software/components/grafite/grafiteAst.ml		diff \| blob \| history
helm/software/components/grafite/grafiteAstPp.ml		diff \| blob \| history
helm/software/components/grafite_engine/grafiteEngine.ml		diff \| blob \| history
helm/software/components/grafite_parser/grafiteParser.ml		diff \| blob \| history
helm/software/components/ng_tactics/nTactics.ml		diff \| blob \| history
helm/software/components/ng_tactics/nTactics.mli		diff \| blob \| history
helm/software/matita/tests/a.ma		diff \| blob \| history