projects
/
helm.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
helm.git
2012-02-28
matitaweb
commit by user andrea
commit
|
commitdiff
|
tree
|
snapshot
2012-02-28
matitaweb
commit by user andrea
commit
|
commitdiff
|
tree
|
snapshot
2012-02-28
matitaweb
commit by user andrea
commit
|
commitdiff
|
tree
|
snapshot
2012-02-28
matitaweb
commit by user utente2
commit
|
commitdiff
|
tree
|
snapshot
2012-02-28
matitaweb
commit by user andrea
commit
|
commitdiff
|
tree
|
snapshot
2012-02-27
Ferruccio Guidi
some additions to Basic_2
commit
|
commitdiff
|
tree
|
snapshot
2012-02-27
Ferruccio Guidi
- property S6 of stronfly normalizing terms proved
commit
|
commitdiff
|
tree
|
snapshot
2012-02-24
Ferruccio Guidi
site update
commit
|
commitdiff
|
tree
|
snapshot
2012-02-24
Ferruccio Guidi
- we added a web page (Apps_2) for the checked applicat...
commit
|
commitdiff
|
tree
|
snapshot
2012-02-24
Ferruccio Guidi
- "functional" component moved to Apps_2
commit
|
commitdiff
|
tree
|
snapshot
2012-02-23
matitaweb
commit by user andrea
commit
|
commitdiff
|
tree
|
snapshot
2012-02-23
Wilmer Ricciotti
refiner porting from matita 1.
commit
|
commitdiff
|
tree
|
snapshot
2012-02-22
matitaweb
Integrations
commit
|
commitdiff
|
tree
|
snapshot
2012-02-22
matitaweb
Complete outline. Raw scripts.
commit
|
commitdiff
|
tree
|
snapshot
2012-02-21
Ferruccio Guidi
- more properties on strongly normalizing terms ...
commit
|
commitdiff
|
tree
|
snapshot
2012-02-21
Ferruccio Guidi
- site update
commit
|
commitdiff
|
tree
|
snapshot
2012-02-20
Ferruccio Guidi
additions to Basic_2 ...
commit
|
commitdiff
|
tree
|
snapshot
2012-02-20
Ferruccio Guidi
initial properies of the "same top term constructor...
commit
|
commitdiff
|
tree
|
snapshot
2012-02-18
Ferruccio Guidi
more results on strongly normalizing terms
commit
|
commitdiff
|
tree
|
snapshot
2012-02-14
Ferruccio Guidi
additions to Basic_2
commit
|
commitdiff
|
tree
|
snapshot
2012-02-14
Ferruccio Guidi
- more properties on strongly normalizing terms
commit
|
commitdiff
|
tree
|
snapshot
2012-02-11
Ferruccio Guidi
additions to Basic_2
commit
|
commitdiff
|
tree
|
snapshot
2012-02-11
Ferruccio Guidi
- strong normalization of abbreviation proved
commit
|
commitdiff
|
tree
|
snapshot
2012-02-09
Ferruccio Guidi
- design table for Basic_2
commit
|
commitdiff
|
tree
|
snapshot
2012-02-09
Ferruccio Guidi
- first properties of strongly normalizing terms
commit
|
commitdiff
|
tree
|
snapshot
2012-02-02
Ferruccio Guidi
- one file and three lemmas added to Basic 2
commit
|
commitdiff
|
tree
|
snapshot
2012-02-02
Ferruccio Guidi
- three lemmas on context sensitive parallel reduction...
commit
|
commitdiff
|
tree
|
snapshot
2012-02-01
Ferruccio Guidi
- notation fix for reducible and normal forms
commit
|
commitdiff
|
tree
|
snapshot
2012-02-01
Ferruccio Guidi
the Basic_2 page was not regenerated ...
commit
|
commitdiff
|
tree
|
snapshot
2012-02-01
Ferruccio Guidi
we added summary and timeline to the Basic_2 page
commit
|
commitdiff
|
tree
|
snapshot
2012-01-31
Claudio Sacerdoti...
Notation for destructuring let-in for triples fixed.
commit
|
commitdiff
|
tree
|
snapshot
2012-01-29
Ferruccio Guidi
- transitivity of lenv refinement for atomic arity...
commit
|
commitdiff
|
tree
|
snapshot
2012-01-29
Ferruccio Guidi
more files added to Basic_2
commit
|
commitdiff
|
tree
|
snapshot
2012-01-27
Ferruccio Guidi
support for abstract candidates of reducibility closed...
commit
|
commitdiff
|
tree
|
snapshot
2012-01-27
Ferruccio Guidi
more files added to Basic_2
commit
|
commitdiff
|
tree
|
snapshot
2012-01-27
Wilmer Ricciotti
Fixes a bug in is_flexible (when checking a meta in...
commit
|
commitdiff
|
tree
|
snapshot
2012-01-27
Claudio Sacerdoti...
Better error messages.
commit
|
commitdiff
|
tree
|
snapshot
2012-01-26
Ferruccio Guidi
- one file added to Basic_2
commit
|
commitdiff
|
tree
|
snapshot
2012-01-26
Ferruccio Guidi
- main lemmas about abstract reducibility candidates...
commit
|
commitdiff
|
tree
|
snapshot
2012-01-23
Wilmer Ricciotti
Inversion principles generation falls back to cases...
commit
|
commitdiff
|
tree
|
snapshot
2012-01-21
Ferruccio Guidi
big fixin the structure of Basic_2
commit
|
commitdiff
|
tree
|
snapshot
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
next