| 2009-03-26 |
Enrico Tassi | new apply almost there |
tree | commitdiff |
| 2009-03-16 |
Enrico Tassi | added mactions, the three can now be collapsed to fit... |
tree | commitdiff |
| 2009-03-16 |
Andrea Asperti | Adapted to new applyS. |
tree | commitdiff |
| 2009-03-16 |
Andrea Asperti | Added a property. |
tree | commitdiff |
| 2009-02-16 |
Enrico Tassi | some notational experiments |
tree | commitdiff |
| 2009-02-15 |
Enrico Tassi | minor changes to make the library compile after wilmers... |
tree | commitdiff |
| 2009-02-13 |
Wilmer Ricciotti | Axiomatization of real numbers (work in progress) |
tree | commitdiff |
| 2009-01-28 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-01-26 |
Enrico Tassi | maction support added to notation, adopted for = AKA... |
tree | commitdiff |
| 2008-12-22 |
Enrico Tassi | Some clean up. |
tree | commitdiff |
| 2008-12-21 |
Claudio Sacerdoti... | New category SET (whose objects are setoids). |
tree | commitdiff |
| 2008-12-19 |
Enrico Tassi | fix exponentiation |
tree | commitdiff |
| 2008-12-19 |
Enrico Tassi | fixed, it seems the new handling of hints in some rare... |
tree | commitdiff |
| 2008-12-18 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-12-15 |
Enrico Tassi | use named types to force some constraints asap |
tree | commitdiff |
| 2008-12-09 |
Enrico Tassi | fixed notation |
tree | commitdiff |
| 2008-12-08 |
Claudio Sacerdoti... | A (boring and long) once-in-a-life exercise on proving... |
tree | commitdiff |
| 2008-12-01 |
Enrico Tassi | 0.5.6 almost ok |
tree | commitdiff |
| 2008-12-01 |
Enrico Tassi | all done |
tree | commitdiff |
| 2008-12-01 |
Enrico Tassi | more ex and more notation |
tree | commitdiff |
| 2008-12-01 |
Enrico Tassi | better doc |
tree | commitdiff |
| 2008-11-30 |
Enrico Tassi | natural deduction support for lemmas with premises |
tree | commitdiff |
| 2008-11-24 |
Enrico Tassi | .... |
tree | commitdiff |
| 2008-11-20 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-11-20 |
Enrico Tassi | dama almost ok |
tree | commitdiff |
| 2008-11-20 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-11-20 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-11-20 |
Enrico Tassi | dama into the library |
tree | commitdiff |
| 2008-11-17 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-11-17 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-11-17 |
Enrico Tassi | exercises ready |
tree | commitdiff |
| 2008-11-17 |
Enrico Tassi | all ex done |
tree | commitdiff |
| 2008-11-16 |
Enrico Tassi | fixed |
tree | commitdiff |
| 2008-11-16 |
Enrico Tassi | commented out unfinished proof |
tree | commitdiff |
| 2008-11-15 |
Enrico Tassi | better spacing |
tree | commitdiff |
| 2008-11-15 |
Enrico Tassi | apply rule (lem EM) works |
tree | commitdiff |
| 2008-11-15 |
Claudio Sacerdoti... | New bug. |
tree | commitdiff |
| 2008-11-15 |
Enrico Tassi | fixed or-in-left |
tree | commitdiff |
| 2008-11-15 |
Enrico Tassi | fixed not-e |
tree | commitdiff |
| 2008-11-15 |
Claudio Sacerdoti... | Another bug. |
tree | commitdiff |
| 2008-11-15 |
Claudio Sacerdoti... | This commit shows a bug. |
tree | commitdiff |
| 2008-11-15 |
Enrico Tassi | almost ready |
tree | commitdiff |
| 2008-11-15 |
Enrico Tassi | rules fixed |
tree | commitdiff |
| 2008-11-15 |
Enrico Tassi | make all/clean implemented |
tree | commitdiff |
| 2008-11-15 |
Enrico Tassi | housekeeping |
tree | commitdiff |
| 2008-11-15 |
Enrico Tassi | house keeping |
tree | commitdiff |
| 2008-11-15 |
Enrico Tassi | natural deduction palette |
tree | commitdiff |
| 2008-11-06 |
Enrico Tassi | natural deduction support and example split, seems... |
tree | commitdiff |
| 2008-11-06 |
Enrico Tassi | fixed scripts |
tree | commitdiff |
| 2008-11-05 |
Enrico Tassi | fixed script to use auto depth=4 |
tree | commitdiff |
| 2008-11-04 |
Claudio Sacerdoti... | - A new interesting elimination principle over inductiv... |
tree | commitdiff |
| 2008-10-20 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-09-26 |
Enrico Tassi | fixed some notational collisions |
tree | commitdiff |
| 2008-09-26 |
Enrico Tassi | commented out a line that was making the file fail |
tree | commitdiff |
| 2008-09-25 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2008-09-25 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2008-09-22 |
Enrico Tassi | fixed auto invocation |
tree | commitdiff |
| 2008-09-18 |
Ferruccio Guidi | applyTransformation: improved error detection |
tree | commitdiff |
| 2008-09-18 |
Claudio Sacerdoti... | Major reordering of theorems in the appropriate files. |
tree | commitdiff |
| 2008-09-18 |
Claudio Sacerdoti... | Precedence level of \downarrow changed to match that... |
tree | commitdiff |
| 2008-09-16 |
Claudio Sacerdoti... | formal_map now defined |
tree | commitdiff |
| 2008-09-16 |
Claudio Sacerdoti... | Definition of formal_topologies. |
tree | commitdiff |
| 2008-09-15 |
Claudio Sacerdoti... | BTop is a category. |
tree | commitdiff |
| 2008-09-12 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2008-09-12 |
Claudio Sacerdoti... | 1) as usual, I took the reverse notation for composition. |
tree | commitdiff |
| 2008-09-09 |
Claudio Sacerdoti... | Reordering of lemmas in proper places. |
tree | commitdiff |
| 2008-09-09 |
Claudio Sacerdoti... | Concrete spaces do form a category, after all :-) |
tree | commitdiff |
| 2008-09-09 |
Claudio Sacerdoti... | Getting closer thanks to more technical arrangements. |
tree | commitdiff |
| 2008-09-08 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2008-09-08 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-09-08 |
Claudio Sacerdoti... | Concrete spaces now defined. |
tree | commitdiff |
| 2008-09-05 |
Enrico Tassi | unification+pullback fix. It used to saturate a coercio... |
tree | commitdiff |
| 2008-09-04 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2008-09-04 |
Enrico Tassi | fixed notation |
tree | commitdiff |
| 2008-09-04 |
Enrico Tassi | restored |
tree | commitdiff |
| 2008-09-04 |
Enrico Tassi | .... |
tree | commitdiff |
| 2008-09-04 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-09-04 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2008-09-04 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-09-04 |
Enrico Tassi | removed old non-working file |
tree | commitdiff |
| 2008-09-03 |
Claudio Sacerdoti... | Setoids are now more pervasive. |
tree | commitdiff |
| 2008-08-31 |
Claudio Sacerdoti... | Relations are now closer to Sambin's ones. I.e. they... |
tree | commitdiff |
| 2008-08-28 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-08-27 |
Claudio Sacerdoti... | Convergence is now defined. |
tree | commitdiff |
| 2008-08-27 |
Claudio Sacerdoti... | Better notation, in particular for subset comprehension. |
tree | commitdiff |
| 2008-08-26 |
Claudio Sacerdoti... | Notation |.| moved to core_notation. |
tree | commitdiff |
| 2008-08-25 |
Claudio Sacerdoti... | New categories REL and BP. |
tree | commitdiff |
| 2008-08-25 |
Claudio Sacerdoti... | New cool "type-checking" notation using colors and... |
tree | commitdiff |
| 2008-08-23 |
Claudio Sacerdoti... | Definition of categories. |
tree | commitdiff |
| 2008-08-23 |
Claudio Sacerdoti... | Some notation moved to core_notation. |
tree | commitdiff |
| 2008-08-23 |
Claudio Sacerdoti... | Also create the graphviz graph. |
tree | commitdiff |
| 2008-08-16 |
Enrico Tassi | added interpretation for \naturals, \rationals, and... |
tree | commitdiff |
| 2008-07-23 |
Enrico Tassi | remove bad aliases from toolbox |
tree | commitdiff |
| 2008-07-23 |
Claudio Sacerdoti... | Universe levels fixed. |
tree | commitdiff |
| 2008-07-22 |
Claudio Sacerdoti... | In some universe, membership is a morphism. |
tree | commitdiff |
| 2008-07-22 |
Claudio Sacerdoti... | Sambin's & Valentini's toolbox (???) |
tree | commitdiff |
| 2008-07-22 |
Claudio Sacerdoti... | Dependencies removed. |
tree | commitdiff |
| 2008-07-18 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2008-07-18 |
Claudio Sacerdoti... | New input notation for bottom-up tree construction... |
tree | commitdiff |
| 2008-07-18 |
Claudio Sacerdoti... | Input notation. |
tree | commitdiff |
| next |
projects / helm.git / history