]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d75baa0) | patch
First experimental version of the declarative proof language for Matita.
authormaiorino <??>
Tue, 11 Jul 2006 15:44:46 +0000 (15:44 +0000)
committermaiorino <??>
Tue, 11 Jul 2006 15:44:46 +0000 (15:44 +0000)
commit50fd7ca0b4e54ee341517ea653b3862b9655d4c5
treed695443c7820b2124bf5d6f3de7b4491c0b2746ctree | snapshot
parentd75baa041cdbffe32948b649ffb49af6a0093a1bcommit | diff
First experimental version of the declarative proof language for Matita.
Supported commands so far:
  assume id: term
  suppose term (id)
  by term done
  by term we proved term (id)
  we need to prove term (id)
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/.depend diff | blob | history
helm/software/components/tactics/Makefile diff | blob | history
helm/software/components/tactics/declarative.ml [new file with mode: 0644] blob
helm/software/components/tactics/declarative.mli [new file with mode: 0644] blob
helm/software/matita/tests/decl.ma [new file with mode: 0644] blob
Unnamed repository; edit this file 'description' to name the repository.