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

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

author	Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
	Thu, 30 Nov 2006 15:06:26 +0000 (15:06 +0000)
committer	Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
	Thu, 30 Nov 2006 15:06:26 +0000 (15:06 +0000)
commit	b309e9baa51822004379ce6364e138e5e803efe4
tree	1445cce0ceb8e17cb5eaa13c136cdbb53449ae50	tree \| snapshot
parent	8a219d1957a19d666a929e9a674a5fddee10066b	commit \| diff

New syntax and semantics for the rewriting steps that make the pretty-printed
proof similar to the input proof.

Syntax:

((obtain id | conclude) lhs) = rhs done?

Semantics:
use conclude when working top-down and obtain to work bottom-up.
done means that this was the last step.

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

RSS Atom

components/grafite/grafiteAst.ml		diff \| blob \| history
components/grafite/grafiteAstPp.ml		diff \| blob \| history
components/grafite_parser/grafiteDisambiguate.ml		diff \| blob \| history
components/grafite_parser/grafiteParser.ml		diff \| blob \| history
components/tactics/declarative.ml		diff \| blob \| history
components/tactics/declarative.mli		diff \| blob \| history
matita/matita.lang		diff \| blob \| history
matita/tests/decl.ma		diff \| blob \| history