]> matita.cs.unibo.it Git - helm.git/commit
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
treef93e915b348dffdcfdbe44a833bbdcebe6689bee
parentcca52355d183a00695b9e310b17c8945ae915b64
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]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/makefile
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/plist/defs.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/plist/props.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/theory.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/types/defs.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/dec.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/arity/defs.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ceqc/defs.ma [deleted file]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ceqc/props.ma [deleted file]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csub3/clear.ma [deleted file]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csub3/defs.ma [deleted file]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csub3/drop.ma [deleted file]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csub3/fwd.ma [deleted file]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csub3/getl.ma [deleted file]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csub3/pc3.ma [deleted file]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csub3/props.ma [deleted file]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csub3/ty3.ma [deleted file]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csuba/arity.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csuba/clear.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csuba/defs.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csuba/drop.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csuba/fwd.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csuba/getl.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/arity.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/clear.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/csuba.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/defs.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/drop.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/drop1.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/getl.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/props.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubst1/defs.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubt/clear.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubt/defs.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubt/drop.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubt/fwd.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubt/getl.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubt/pc3.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubt/props.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubt/ty3.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop1/defs.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop1/getl.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop1/props.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/fsubst0/defs.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/defs.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/fwd.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/leq/defs.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/defs.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/props.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift1/fwd.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift1/props.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/makefile
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pc3/defs.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/fwd.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr2/props.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr3/defs.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr3/fwd.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr3/iso.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/arity.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/props.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sn3/defs.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sn3/fwd.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sn3/props.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/fwd.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst1/defs.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tau0/defs.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tau1/defs.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tlist/defs.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tlist/props.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/defs.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/pr3.ma