]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 07d0680) | 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)
commit6995a7717fd0c760c0608ed9225e9f2dbc14d7d1
treeab7fe4a73a93f1bdffa492ec64d46e011dc829a0tree | snapshot
parent07d068011fb816e94a14056ab1058c796312606bcommit | 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)
components/grafite/grafiteAst.ml diff | blob | history
components/grafite/grafiteAstPp.ml diff | blob | history
components/grafite_engine/grafiteEngine.ml diff | blob | history
components/grafite_parser/grafiteDisambiguate.ml diff | blob | history
components/grafite_parser/grafiteParser.ml diff | blob | history
components/tactics/.depend diff | blob | history
components/tactics/Makefile diff | blob | history
components/tactics/declarative.ml [new file with mode: 0644] blob
components/tactics/declarative.mli [new file with mode: 0644] blob
matita/tests/decl.ma [new file with mode: 0644] blob
Unnamed repository; edit this file 'description' to name the repository.