]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 93cc2a2) | patch
demodulate takes an extra argument 'all', if present it attempts to solve
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 22 Apr 2009 10:30:55 +0000 (10:30 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 22 Apr 2009 10:30:55 +0000 (10:30 +0000)
commit5c10d402b5de7233bc83d7f685b274832e383212
tree62a51112242bd24215912f9b8a0cc41b86dfdc36tree | snapshot
parent93cc2a2254a2620000377dfc99a7aaedf2b8ec63commit | diff
demodulate takes an extra argument 'all', if present it attempts to solve
the goal demodulating it in any possible way. an extra steps argument may
be used to increase the default maximum number of demodulation steps (1).
pump may also affect the result.
helm/software/components/grafite_parser/grafiteParser.ml diff | blob | history
helm/software/components/tactics/auto.ml diff | blob | history
helm/software/components/tactics/declarative.ml diff | blob | history
helm/software/components/tactics/paramodulation/indexing.ml diff | blob | history
helm/software/matita/library/demo/propositional_sequent_calculus.ma diff | blob | history
helm/software/matita/library/nat/div_and_mod.ma diff | blob | history
helm/software/matita/library/nat/minus.ma diff | blob | history
helm/software/matita/library/nat/times.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.