projects
/
helm.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
helm.git
2012-01-21
Ferruccio Guidi
more files to Basic_2
commit
|
commitdiff
|
tree
|
snapshot
2012-01-21
Ferruccio Guidi
- main proof for strong normalization closed! ...
commit
|
commitdiff
|
tree
|
snapshot
2012-01-19
Ferruccio Guidi
closure property S4 added to abstract candidates of...
commit
|
commitdiff
|
tree
|
snapshot
2012-01-16
Ferruccio Guidi
the support for candidates of reducibility continues ...
commit
|
commitdiff
|
tree
|
snapshot
2012-01-16
Ferruccio Guidi
some additionsand refactoring in Basic_2
commit
|
commitdiff
|
tree
|
snapshot
2012-01-13
Ferruccio Guidi
more file names added to Basic_2
commit
|
commitdiff
|
tree
|
snapshot
2012-01-13
Ferruccio Guidi
- the development of abstract reducibility candidates...
commit
|
commitdiff
|
tree
|
snapshot
2012-01-12
Wilmer Ricciotti
Improves the presentation of hypotheses in the goal...
commit
|
commitdiff
|
tree
|
snapshot
2012-01-11
Wilmer Ricciotti
Fixes r11788 (partial, thus broken commit).
commit
|
commitdiff
|
tree
|
snapshot
2012-01-10
Ferruccio Guidi
unpatched version for the new CamplP5
commit
|
commitdiff
|
tree
|
snapshot
2012-01-10
Ferruccio Guidi
patched version for old CamlP5
commit
|
commitdiff
|
tree
|
snapshot
2012-01-10
Wilmer Ricciotti
Bugfix: NCicUnification.could_reduce now performs whd...
commit
|
commitdiff
|
tree
|
snapshot
2012-01-10
Andrea Asperti
A complete snapshot for re
commit
|
commitdiff
|
tree
|
snapshot
2012-01-08
Ferruccio Guidi
more characters shortcuts
commit
|
commitdiff
|
tree
|
snapshot
2012-01-08
Ferruccio Guidi
Basic_2: restyling and more notation
commit
|
commitdiff
|
tree
|
snapshot
2012-01-08
Ferruccio Guidi
- notation restyling ...
commit
|
commitdiff
|
tree
|
snapshot
2012-01-07
Ferruccio Guidi
Basic_2: - we addedsome files
commit
|
commitdiff
|
tree
|
snapshot
2012-01-07
Ferruccio Guidi
lambda_delta: global environments handling: redefined...
commit
|
commitdiff
|
tree
|
snapshot
2012-01-04
Ferruccio Guidi
the support for reducibility candidates evolves ,,,,
commit
|
commitdiff
|
tree
|
snapshot
2012-01-03
Andrea Asperti
Complete version
commit
|
commitdiff
|
tree
|
snapshot
2012-01-03
Andrea Asperti
modified definition of memb
commit
|
commitdiff
|
tree
|
snapshot
2012-01-03
Andrea Asperti
reverse
commit
|
commitdiff
|
tree
|
snapshot
2012-01-03
Andrea Asperti
more properties of union
commit
|
commitdiff
|
tree
|
snapshot
2012-01-03
Andrea Asperti
noteq_to_eqnot
commit
|
commitdiff
|
tree
|
snapshot
2011-12-26
Ferruccio Guidi
notation and dependences bug fix
commit
|
commitdiff
|
tree
|
snapshot
2011-12-25
Ferruccio Guidi
Basic 2 page update
commit
|
commitdiff
|
tree
|
snapshot
2011-12-25
Ferruccio Guidi
- support for candidates of reducibility continues ...
commit
|
commitdiff
|
tree
|
snapshot
2011-12-20
Ferruccio Guidi
Basic_2 update ...
commit
|
commitdiff
|
tree
|
snapshot
2011-12-20
Ferruccio Guidi
- the definition of the framework for strong normalizat...
commit
|
commitdiff
|
tree
|
snapshot
2011-12-16
Andrea Asperti
In case paramodulation fails we apply unit equalities.
commit
|
commitdiff
|
tree
|
snapshot
2011-12-15
Andrea Asperti
Splitted DeqSets in their own file. Notation for memb...
commit
|
commitdiff
|
tree
|
snapshot
2011-12-15
Andrea Asperti
Hints sui DeqSets
commit
|
commitdiff
|
tree
|
snapshot
2011-12-14
Claudio Sacerdoti...
More stuff from CerCo to the standard library.
commit
|
commitdiff
|
tree
|
snapshot
2011-12-14
Claudio Sacerdoti...
Some more lemmas from CerCo.
commit
|
commitdiff
|
tree
|
snapshot
2011-12-14
Wilmer Ricciotti
Matitaweb: large commit porting to the new Matita 0...
commit
|
commitdiff
|
tree
|
snapshot
2011-12-14
Claudio Sacerdoti...
1) Notation for dependent pairs differentiated from...
commit
|
commitdiff
|
tree
|
snapshot
2011-12-13
Claudio Sacerdoti...
Dependent pairs (i.e. Sigma types in Type[0]) are back...
commit
|
commitdiff
|
tree
|
snapshot
2011-12-13
Claudio Sacerdoti...
1) PSig and Sig merged into a single Sigma type in...
commit
|
commitdiff
|
tree
|
snapshot
2011-12-13
Claudio Sacerdoti...
inject/eject replaced by mk_Sig/pi1.
commit
|
commitdiff
|
tree
|
snapshot
2011-12-13
Claudio Sacerdoti...
1) New file russell with the coercions to activate...
commit
|
commitdiff
|
tree
|
snapshot
2011-12-13
matitaweb
Chapter 5 = re.ma ; chapter 6 = moves.ma
commit
|
commitdiff
|
tree
|
snapshot
2011-12-13
matitaweb
New chapter 4
commit
|
commitdiff
|
tree
|
snapshot
2011-12-13
Wilmer Ricciotti
Matitaweb: clicking buttons disables the GUI to prevent...
commit
|
commitdiff
|
tree
|
snapshot
2011-12-13
Andrea Asperti
Splitted re into lang.ma nd re.ma
commit
|
commitdiff
|
tree
|
snapshot
2011-12-13
Andrea Asperti
Sig in Prop
commit
|
commitdiff
|
tree
|
snapshot
2011-12-13
Claudio Sacerdoti...
More stuff integrated from CerCo on sigma types (that...
commit
|
commitdiff
|
tree
|
snapshot
2011-12-13
Enrico Tassi
axiom-
commit
|
commitdiff
|
tree
|
snapshot
2011-12-12
Claudio Sacerdoti...
pair => mk_Prod (one more was left in notation)
commit
|
commitdiff
|
tree
|
snapshot
2011-12-12
Claudio Sacerdoti...
precedence level of if-then-else fixed
commit
|
commitdiff
|
tree
|
snapshot
2011-12-12
Claudio Sacerdoti...
Added elimination principles for destructuring let...
commit
|
commitdiff
|
tree
|
snapshot
2011-12-12
Claudio Sacerdoti...
Some integrations from CerCo. In particular:
commit
|
commitdiff
|
tree
|
snapshot
2011-12-12
Enrico Tassi
support -axiom to avoind indexing an axiom (since there...
commit
|
commitdiff
|
tree
|
snapshot
2011-12-12
Ferruccio Guidi
- we improved and updated the generated web pages
commit
|
commitdiff
|
tree
|
snapshot
2011-12-12
Claudio Sacerdoti...
Pairs are now records.
commit
|
commitdiff
|
tree
|
snapshot
2011-12-12
Claudio Sacerdoti...
Parentheses are now needed. I do not know why and when...
commit
|
commitdiff
|
tree
|
snapshot
2011-12-12
Wilmer Ricciotti
Matitaweb: changes to matitadaemon.ml to make it work...
commit
|
commitdiff
|
tree
|
snapshot
2011-12-12
Wilmer Ricciotti
Matitaweb: added utility for conversion of user dbs...
commit
|
commitdiff
|
tree
|
snapshot
2011-12-12
Claudio Sacerdoti...
Re-Ported to
commit
|
commitdiff
|
tree
|
snapshot
2011-12-12
Wilmer Ricciotti
Matitaweb: secure SHA-256 encryption for passwords.
commit
|
commitdiff
|
tree
|
snapshot
2011-12-12
matitaweb
commit by user andrea
commit
|
commitdiff
|
tree
|
snapshot
2011-12-12
matitaweb
commit by user andrea
commit
|
commitdiff
|
tree
|
snapshot
2011-12-12
matitaweb
commit by user andrea
commit
|
commitdiff
|
tree
|
snapshot
2011-12-12
matitaweb
commit by user andrea
commit
|
commitdiff
|
tree
|
snapshot
2011-12-12
Ferruccio Guidi
nat library reorganized ....
commit
|
commitdiff
|
tree
|
snapshot
2011-12-12
Andrea Asperti
Generalization to any alphabet. We do not need a finite
commit
|
commitdiff
|
tree
|
snapshot
2011-12-11
Ferruccio Guidi
- slicing relation for the global environment defined...
commit
|
commitdiff
|
tree
|
snapshot
2011-12-09
Andrea Asperti
list.ma moved inside lists.
commit
|
commitdiff
|
tree
|
snapshot
2011-12-09
Andrea Asperti
closing more axioms
commit
|
commitdiff
|
tree
|
snapshot
2011-12-08
Ferruccio Guidi
updating the information on lambda_delta
commit
|
commitdiff
|
tree
|
snapshot
2011-12-08
Ferruccio Guidi
Maietty suggested to change a paragraph on the devel...
commit
|
commitdiff
|
tree
|
snapshot
2011-12-08
Ferruccio Guidi
Maietti suggested to replace a paragraph about the...
commit
|
commitdiff
|
tree
|
snapshot
2011-12-07
Andrea Asperti
Closing some axioms...
commit
|
commitdiff
|
tree
|
snapshot
2011-12-07
Andrea Asperti
\vee notation for boolean or
commit
|
commitdiff
|
tree
|
snapshot
2011-12-06
Ferruccio Guidi
new files started ...
commit
|
commitdiff
|
tree
|
snapshot
2011-12-06
Ferruccio Guidi
other addition to the standard library removed
commit
|
commitdiff
|
tree
|
snapshot
2011-12-06
Ferruccio Guidi
we added a definition and a couple of lemmas
commit
|
commitdiff
|
tree
|
snapshot
2011-12-06
Ferruccio Guidi
- support for atomic arities and candidates of reducibi...
commit
|
commitdiff
|
tree
|
snapshot
2011-12-06
Wilmer Ricciotti
Grammar change: let corecs can take no arguments (and...
commit
|
commitdiff
|
tree
|
snapshot
2011-12-06
Wilmer Ricciotti
Fixes a bug that overwrited the index of the recursive...
commit
|
commitdiff
|
tree
|
snapshot
2011-12-06
Andrea Asperti
Listb contains some boolean functions over lists.
commit
|
commitdiff
|
tree
|
snapshot
2011-12-06
Wilmer Ricciotti
Matitaweb:
commit
|
commitdiff
|
tree
|
snapshot
2011-12-06
Andrea Asperti
naive sets (A-> Prop)
commit
|
commitdiff
|
tree
|
snapshot
2011-12-05
Andrea Asperti
More properties of iff
commit
|
commitdiff
|
tree
|
snapshot
2011-12-05
Andrea Asperti
Decidability of equality (draft)
commit
|
commitdiff
|
tree
|
snapshot
2011-11-26
Ferruccio Guidi
component "reducibility" updated to new syntax!
commit
|
commitdiff
|
tree
|
snapshot
2011-11-26
Ferruccio Guidi
component "unfold" updated to new syntax ...
commit
|
commitdiff
|
tree
|
snapshot
2011-11-26
Ferruccio Guidi
component "substitution" updated to new syntax ...
commit
|
commitdiff
|
tree
|
snapshot
2011-11-26
Ferruccio Guidi
- "grammar" component updated to new syntax ...
commit
|
commitdiff
|
tree
|
snapshot
2011-11-25
Ferruccio Guidi
Ground_2 ported to new syntax ...
commit
|
commitdiff
|
tree
|
snapshot
2011-11-25
Ferruccio Guidi
bugfix in clearing the replaced variable: a relocation...
commit
|
commitdiff
|
tree
|
snapshot
2011-11-24
Ferruccio Guidi
Destruct: we warn about the substituted variable to...
commit
|
commitdiff
|
tree
|
snapshot
2011-11-24
Ferruccio Guidi
- now destruct tries to clear the replaced variables...
commit
|
commitdiff
|
tree
|
snapshot
2011-11-24
Enrico Tassi
fixed DESTDIR
commit
|
commitdiff
|
tree
|
snapshot
2011-11-24
Enrico Tassi
fixed DESTDIR
commit
|
commitdiff
|
tree
|
snapshot
2011-11-22
Claudio Sacerdoti...
Changes to disambiguation:
commit
|
commitdiff
|
tree
|
snapshot
2011-11-21
Ferruccio Guidi
Basic_2 file names update
commit
|
commitdiff
|
tree
|
snapshot
2011-11-21
Claudio Sacerdoti...
Syntax change: change where what => change what where.
commit
|
commitdiff
|
tree
|
snapshot
2011-11-21
Andrea Asperti
regular expressions
commit
|
commitdiff
|
tree
|
snapshot
2011-11-21
Andrea Asperti
Filtering all equations that cannot be embedded (contai...
commit
|
commitdiff
|
tree
|
snapshot
2011-11-21
Andrea Asperti
Passing the correct subst a metasenv when idexing local...
commit
|
commitdiff
|
tree
|
snapshot
next