]> 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)
commit1beb5e1624ac1db045e36dff93d0cfafa6a70995
treee4e08cf68f3a758b444f32ae5dfffac47c8aeb7b
parented5b072125435beb688d4da148fd3b09f849658a
- 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:
components/grafite/grafiteAst.ml
components/grafite/grafiteAstPp.ml
components/grafite_engine/grafiteEngine.ml
components/grafite_parser/grafiteParser.ml
components/tactics/Makefile
components/tactics/eliminationTactics.ml
components/tactics/eliminationTactics.mli
components/tactics/equalityTactics.ml
components/tactics/fwdSimplTactic.ml
components/tactics/proofEngineStructuralRules.ml
components/tactics/proofEngineStructuralRules.mli
components/tactics/ring.ml
components/tactics/tactics.mli
matita/contribs/RELATIONAL-ARITHMETICS/add_fwd.ma
matita/contribs/RELATIONAL-ARITHMETICS/add_props.ma
matita/contribs/RELATIONAL-ARITHMETICS/nat_fwd.ma
matita/help/C/sec_tactics.xml
matita/help/C/tactic_quickref.xml