]> matita.cs.unibo.it Git - helm.git/commit - helm/ocaml/tactics/tactics.ml
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b92a0ec) | patch
New tactic: inversion.
authormarangon <??>
Thu, 15 Dec 2005 16:02:48 +0000 (16:02 +0000)
committermarangon <??>
Thu, 15 Dec 2005 16:02:48 +0000 (16:02 +0000)
commit059c1bb4766e823aa53b39fed7d3dd55b4a06101
tree9c08b81c999d03e9e5293947202c44106d876ceatree | snapshot
parentb92a0ec32215eea5e0452154da54d5a29a84a53ecommit | diff
New tactic: inversion.
 - only first phase implemented (no cleaning)
 - code in inversion.ml to be improved/cleaned up
helm/ocaml/grafite/grafiteAst.ml diff | blob | history
helm/ocaml/grafite/grafiteAstPp.ml diff | blob | history
helm/ocaml/grafite2/grafiteEngine.ml diff | blob | history
helm/ocaml/grafite_parser/grafiteDisambiguate.ml diff | blob | history
helm/ocaml/grafite_parser/grafiteParser.ml diff | blob | history
helm/ocaml/tactics/.depend diff | blob | history
helm/ocaml/tactics/Makefile diff | blob | history
helm/ocaml/tactics/inversion.ml [new file with mode: 0644] blob
helm/ocaml/tactics/inversion.mli [new file with mode: 0644] blob
helm/ocaml/tactics/tactics.ml diff | blob | history
helm/ocaml/tactics/tactics.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.