]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2bfd692) | patch
- tactics:
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 29 Dec 2006 11:28:13 +0000 (11:28 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 29 Dec 2006 11:28:13 +0000 (11:28 +0000)
commit5f00ef380aafdaae93a40a3a47491d43ec9c3a62
tree48200a6cc14d4dcf9635f67fd81e50a49b0f8e5ctree | snapshot
parent2bfd692efc9b2c41d67d31bf36801d150f5715fccommit | diff
- tactics:
  rename tactic enabled,
  rewrite and rewrite_simpl now take optional names for the rewrited premises
- procedural script reconstruction
  now starts directly from acic bypassing the content level,
  the script for the use case proof in matita/contribs/prova.ma is reconstructed  completely now and is correctly parsed and typechecked
27 files changed:
helm/software/components/content_pres/.depend diff | blob | history
helm/software/components/content_pres/Makefile diff | blob | history
helm/software/components/content_pres/acic2Procedural.ml [new file with mode: 0644] blob
helm/software/components/content_pres/acic2Procedural.mli [new file with mode: 0644] blob
helm/software/components/content_pres/cicClassify.ml [new file with mode: 0644] blob
helm/software/components/content_pres/cicClassify.mli [new file with mode: 0644] blob
helm/software/components/content_pres/content2Procedural.ml [deleted file] blob | history
helm/software/components/content_pres/content2Procedural.mli [deleted file] blob | history
helm/software/components/content_pres/objPp.ml diff | blob | history
helm/software/components/content_pres/proceduralTypes.ml [new file with mode: 0644] blob
helm/software/components/content_pres/proceduralTypes.mli [new file with mode: 0644] blob
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/grafiteDisambiguate.ml diff | blob | history
helm/software/components/grafite_parser/grafiteParser.ml diff | blob | history
helm/software/components/tactics/auto.ml diff | blob | history
helm/software/components/tactics/discriminationTactics.ml diff | blob | history
helm/software/components/tactics/equalityTactics.ml diff | blob | history
helm/software/components/tactics/equalityTactics.mli diff | blob | history
helm/software/components/tactics/fourierR.ml diff | blob | history
helm/software/components/tactics/proofEngineStructuralRules.ml diff | blob | history
helm/software/components/tactics/proofEngineStructuralRules.mli diff | blob | history
helm/software/components/tactics/tactics.ml diff | blob | history
helm/software/components/tactics/tactics.mli diff | blob | history
helm/software/matita/contribs/prova.ma diff | blob | history
helm/software/matita/matita.lang diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.