]> matita.cs.unibo.it Git - helm.git/commit
- matitaInit matitaprover matitadep matitamake:
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 5 Sep 2007 13:50:38 +0000 (13:50 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 5 Sep 2007 13:50:38 +0000 (13:50 +0000)
commit15d6dc1249038e9235bb0f776f2c5ae0b37f17f1
tree90495dc35d392a4a34e89088d8d02546bfbb0c9c
parent033ef07477e15b36c2865f91c0ccf139a66e6fd7
- matitaInit matitaprover matitadep matitamake:
  fixed configuration precedence:
  cmdline > configuration_file > default
- core_natation:
  added notation for single step parallel reduction: =>
- LAMBDA-TYPES: some new theorems
- LOGIC: some new definitions
36 files changed:
matita/contribs/LAMBDA-TYPES/Base-1/ext/arith.ma
matita/contribs/LAMBDA-TYPES/Base-1/makefile
matita/contribs/LAMBDA-TYPES/Base-1/preamble.ma
matita/contribs/LAMBDA-TYPES/Base-1/spare.ma
matita/contribs/LAMBDA-TYPES/Base-1/types/defs.ma
matita/contribs/LAMBDA-TYPES/Base-2/blt/defs.mma
matita/contribs/LAMBDA-TYPES/Base-2/ext/arith.mma
matita/contribs/LAMBDA-TYPES/Base-2/plist/defs.mma
matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma
matita/contribs/LAMBDA-TYPES/Base-2/types/defs.mma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/props.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/definitions.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex2/defs.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex2/props.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/asucc.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/props.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/makefile
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/arity.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/defs.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/fwd.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/props.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/fwd.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/spare.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/theory.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity_props.ma
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/nf2.ma [new file with mode: 0644]
matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/props.ma
matita/contribs/LOGIC/PNF/defs.ma [new file with mode: 0644]
matita/contribs/LOGIC/PRed/defs.ma [new file with mode: 0644]
matita/core_notation.moo
matita/matitaInit.ml
matita/matitaInit.mli
matita/matitadep.ml
matita/matitamake.ml
matita/matitaprover.ml