]> matita.cs.unibo.it Git - helm.git/commit
- decompose now runs with no arguments (operates on the whole context)
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 27 Jun 2006 16:57:46 +0000 (16:57 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 27 Jun 2006 16:57:46 +0000 (16:57 +0000)
commitcc3ab906b631ef0edb4402cb622fc3fa96682717
tree85c141ab7d6e1984bbfa5fdf588a68ef4d8db019
parent44f4e888646ac95752bbd8c3e7b9b4b48209b1a6
- decompose now runs with no arguments (operates on the whole context)
- clear now takes a list of hypotheses (clears each)
- RELATIONAL-ARITHMETICS updated to use the new tactics
- tactics/Makefile fixed to correctly build tactics.mli
18 files changed:
helm/software/components/grafite/grafiteAst.ml
helm/software/components/grafite/grafiteAstPp.ml
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/grafite_parser/grafiteParser.ml
helm/software/components/tactics/Makefile
helm/software/components/tactics/eliminationTactics.ml
helm/software/components/tactics/eliminationTactics.mli
helm/software/components/tactics/equalityTactics.ml
helm/software/components/tactics/fwdSimplTactic.ml
helm/software/components/tactics/proofEngineStructuralRules.ml
helm/software/components/tactics/proofEngineStructuralRules.mli
helm/software/components/tactics/ring.ml
helm/software/components/tactics/tactics.mli
helm/software/matita/contribs/RELATIONAL-ARITHMETICS/add_fwd.ma
helm/software/matita/contribs/RELATIONAL-ARITHMETICS/add_props.ma
helm/software/matita/contribs/RELATIONAL-ARITHMETICS/nat_fwd.ma
helm/software/matita/help/C/sec_tactics.xml
helm/software/matita/help/C/tactic_quickref.xml