]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: cca5235) | patch
new theorems added. does not comile well yet :(( problems found in
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 7 Dec 2006 15:43:42 +0000 (15:43 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 7 Dec 2006 15:43:42 +0000 (15:43 +0000)
commit9408f2869ddbbbae68dcb23ebf6c358c61888d0d
treef93e915b348dffdcfdbe44a833bbdcebe6689beetree | snapshot
parentcca52355d183a00695b9e310b17c8945ae915b64commit | diff
new theorems added. does not comile well yet :(( problems found in
- csubc/csuba.ml (exception "List.nth" raised by matitaGui.ml at line 244)
- ty3/pr3.ml (matitac.opt returns with exit code 3 without evident error)
- sn3/props.ma (assertion failure raised by discrimination_tree.ml at line 62)
75 files changed:
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/plist.ma [deleted file] blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/makefile diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/plist/defs.ma [new file with mode: 0644] blob
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/plist/props.ma [new file with mode: 0644] blob
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/theory.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/types/defs.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/dec.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/arity/defs.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ceqc/defs.ma [deleted file] blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ceqc/props.ma [deleted file] blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csub3/clear.ma [deleted file] blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csub3/defs.ma [deleted file] blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csub3/drop.ma [deleted file] blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csub3/fwd.ma [deleted file] blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csub3/getl.ma [deleted file] blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csub3/pc3.ma [deleted file] blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csub3/props.ma [deleted file] blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csub3/ty3.ma [deleted file] blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csuba/arity.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csuba/clear.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csuba/defs.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csuba/drop.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csuba/fwd.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csuba/getl.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/arity.ma [new file with mode: 0644] blob
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/clear.ma [new file with mode: 0644] blob
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/csuba.ma [new file with mode: 0644] blob
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/defs.ma [new file with mode: 0644] blob
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/drop.ma [new file with mode: 0644] blob
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/drop1.ma [new file with mode: 0644] blob
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/getl.ma [new file with mode: 0644] blob
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/props.ma [new file with mode: 0644] blob
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubst1/defs.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubt/clear.ma [new file with mode: 0644] blob
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubt/defs.ma [new file with mode: 0644] blob
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubt/drop.ma [new file with mode: 0644] blob
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubt/fwd.ma [new file with mode: 0644] blob
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubt/getl.ma [new file with mode: 0644] blob
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubt/pc3.ma [new file with mode: 0644] blob
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubt/props.ma [new file with mode: 0644] blob
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubt/ty3.ma [new file with mode: 0644] blob
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop1/defs.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop1/getl.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop1/props.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/fsubst0/defs.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/defs.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/fwd.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/leq/defs.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/defs.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/props.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift1/fwd.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift1/props.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/makefile diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pc3/defs.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/fwd.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr2/props.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr3/defs.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr3/fwd.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr3/iso.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/arity.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/props.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sn3/defs.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sn3/fwd.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sn3/props.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/fwd.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst1/defs.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tau0/defs.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tau1/defs.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tlist/defs.ma [new file with mode: 0644] blob
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tlist/props.ma [new file with mode: 0644] blob
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/defs.ma diff | blob | history
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/pr3.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.