2008-07-02 |
Ferruccio Guidi | svn:ignore set on LambdaDelta-2 |
commit | commitdiff | tree | snapshot |
2008-07-02 |
Ferruccio Guidi | - new tactic applyP for use in the *P*rocedural script... |
commit | commitdiff | tree | snapshot |
2008-07-02 |
Wilmer Ricciotti | Fixed a bug which prevented mutually recursive definiti... |
commit | commitdiff | tree | snapshot |
2008-07-02 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-07-02 |
Enrico Tassi | return 1 in case of failure |
commit | commitdiff | tree | snapshot |
2008-07-02 |
Enrico Tassi | 0.5.2 |
commit | commitdiff | tree | snapshot |
2008-07-02 |
Enrico Tassi | 0.5.2 |
commit | commitdiff | tree | snapshot |
2008-07-02 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-07-02 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-07-02 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-07-02 |
Enrico Tassi | calculation of the sort user to choose the rewriting... |
commit | commitdiff | tree | snapshot |
2008-07-01 |
Ferruccio Guidi | - lambda-delta: some speed up (not very much :) actually) |
commit | commitdiff | tree | snapshot |
2008-07-01 |
Enrico Tassi | shifting done, merge attacked |
commit | commitdiff | tree | snapshot |
2008-07-01 |
Enrico Tassi | shift almost done |
commit | commitdiff | tree | snapshot |
2008-06-30 |
Enrico Tassi | new specification |
commit | commitdiff | tree | snapshot |
2008-06-30 |
Ferruccio Guidi | we improved the data structures used in the translation... |
commit | commitdiff | tree | snapshot |
2008-06-30 |
Enrico Tassi | some more work on q |
commit | commitdiff | tree | snapshot |
2008-06-30 |
Ferruccio Guidi | we tranlate an Automath book in an itermediate format... |
commit | commitdiff | tree | snapshot |
2008-06-28 |
Enrico Tassi | some more work to factorize out uninteresting parts... |
commit | commitdiff | tree | snapshot |
2008-06-27 |
Enrico Tassi | more work to try to understand where the issue is |
commit | commitdiff | tree | snapshot |
2008-06-27 |
Enrico Tassi | lost in the wood |
commit | commitdiff | tree | snapshot |
2008-06-26 |
Enrico Tassi | more work |
commit | commitdiff | tree | snapshot |
2008-06-26 |
Enrico Tassi | few more steps |
commit | commitdiff | tree | snapshot |
2008-06-26 |
Enrico Tassi | more work |
commit | commitdiff | tree | snapshot |
2008-06-26 |
Enrico Tassi | some more work |
commit | commitdiff | tree | snapshot |
2008-06-26 |
Enrico Tassi | more work on q |
commit | commitdiff | tree | snapshot |
2008-06-25 |
Enrico Tassi | some more work |
commit | commitdiff | tree | snapshot |
2008-06-25 |
Enrico Tassi | better, reparsable, notation |
commit | commitdiff | tree | snapshot |
2008-06-24 |
Enrico Tassi | removed <_,_> notation second interpretation for depend... |
commit | commitdiff | tree | snapshot |
2008-06-24 |
Enrico Tassi | notation factored, coercion commant taking terms and... |
commit | commitdiff | tree | snapshot |
2008-06-24 |
Enrico Tassi | missing file added |
commit | commitdiff | tree | snapshot |
2008-06-23 |
Ferruccio Guidi | metaAut.xlate_item started |
commit | commitdiff | tree | snapshot |
2008-06-23 |
Ferruccio Guidi | we set the http daemon timeout to 15 minutes, which... |
commit | commitdiff | tree | snapshot |
2008-06-23 |
Enrico Tassi | more work, but russell too slow |
commit | commitdiff | tree | snapshot |
2008-06-23 |
Enrico Tassi | add \\ in front of tex macros |
commit | commitdiff | tree | snapshot |
2008-06-23 |
Enrico Tassi | notation support fixed to parentesize in a more sane... |
commit | commitdiff | tree | snapshot |
2008-06-23 |
Ferruccio Guidi | stylesheet application moved after header send |
commit | commitdiff | tree | snapshot |
2008-06-23 |
Enrico Tassi | xxx |
commit | commitdiff | tree | snapshot |
2008-06-22 |
Ferruccio Guidi | - grafiteParser.ml: the callback invocation was displaced |
commit | commitdiff | tree | snapshot |
2008-06-20 |
Enrico Tassi | left -> right |
commit | commitdiff | tree | snapshot |
2008-06-20 |
Claudio Sacerdoti... | Fixed bugs in the documentation of notation. |
commit | commitdiff | tree | snapshot |
2008-06-20 |
Claudio Sacerdoti... | More documentation for notation. |
commit | commitdiff | tree | snapshot |
2008-06-20 |
Claudio Sacerdoti... | Further documentation for notation. |
commit | commitdiff | tree | snapshot |
2008-06-20 |
Claudio Sacerdoti... | - partial implementation of pattern for case documented |
commit | commitdiff | tree | snapshot |
2008-06-19 |
Enrico Tassi | fixed core notation |
commit | commitdiff | tree | snapshot |
2008-06-19 |
Enrico Tassi | notation fixed to be NON associative by default |
commit | commitdiff | tree | snapshot |
2008-06-19 |
Claudio Sacerdoti... | 1. bug fixed in generalize_pattern: a lazy const_tac... |
commit | commitdiff | tree | snapshot |
2008-06-19 |
Claudio Sacerdoti... | - notation fixed according to the new stricter semantics |
commit | commitdiff | tree | snapshot |
2008-06-19 |
Ferruccio Guidi | - Procedural: we now check that an eliminator opens... |
commit | commitdiff | tree | snapshot |
2008-06-19 |
Enrico Tassi | notation on steroids: 'term 40 x' is a valid variable... |
commit | commitdiff | tree | snapshot |
2008-06-18 |
Claudio Sacerdoti... | interpretation documented |
commit | commitdiff | tree | snapshot |
2008-06-18 |
Enrico Tassi | initial support for notation that specifies the precede... |
commit | commitdiff | tree | snapshot |
2008-06-18 |
Enrico Tassi | removed unused variable |
commit | commitdiff | tree | snapshot |
2008-06-18 |
Enrico Tassi | some work on Q |
commit | commitdiff | tree | snapshot |
2008-06-17 |
Enrico Tassi | general reorganization and first (unconditional) proof... |
commit | commitdiff | tree | snapshot |
2008-06-17 |
Enrico Tassi | reordering of lexicon status partially avoided to make... |
commit | commitdiff | tree | snapshot |
2008-06-16 |
Ferruccio Guidi | transformation from automath to intermediate language... |
commit | commitdiff | tree | snapshot |
2008-06-16 |
Enrico Tassi | Dedekind sigma completeness for the natural numbers. |
commit | commitdiff | tree | snapshot |
2008-06-16 |
Enrico Tassi | typo |
commit | commitdiff | tree | snapshot |
2008-06-13 |
Enrico Tassi | some notation added with a bit PITA |
commit | commitdiff | tree | snapshot |
2008-06-13 |
Wilmer Ricciotti | final relevance check |
commit | commitdiff | tree | snapshot |
2008-06-13 |
Ferruccio Guidi | copyright information added in the grundlagen text |
commit | commitdiff | tree | snapshot |
2008-06-13 |
Enrico Tassi | when -debug do not catch |
commit | commitdiff | tree | snapshot |
2008-06-13 |
Enrico Tassi | when -debug do not catch |
commit | commitdiff | tree | snapshot |
2008-06-13 |
Enrico Tassi | replace assert false with AssertFailure |
commit | commitdiff | tree | snapshot |
2008-06-13 |
Ferruccio Guidi | Initial version of the Helena Checker |
commit | commitdiff | tree | snapshot |
2008-06-13 |
Claudio Sacerdoti... | New lemma |
commit | commitdiff | tree | snapshot |
2008-06-13 |
Enrico Tassi | more notation |
commit | commitdiff | tree | snapshot |
2008-06-13 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-06-13 |
Enrico Tassi | print the name not found in the env |
commit | commitdiff | tree | snapshot |
2008-06-12 |
Enrico Tassi | Testing some performance tricks by caching the list... |
commit | commitdiff | tree | snapshot |
2008-06-12 |
Enrico Tassi | better names in a lemma to increase readability |
commit | commitdiff | tree | snapshot |
2008-06-12 |
Enrico Tassi | fixed some regressions |
commit | commitdiff | tree | snapshot |
2008-06-11 |
Claudio Sacerdoti... | New, much faster implementation of factorize. |
commit | commitdiff | tree | snapshot |
2008-06-11 |
Enrico Tassi | gran casino |
commit | commitdiff | tree | snapshot |
2008-06-11 |
Enrico Tassi | meta not considered before in outtype |
commit | commitdiff | tree | snapshot |
2008-06-10 |
Enrico Tassi | bla bla bla |
commit | commitdiff | tree | snapshot |
2008-06-10 |
Wilmer Ricciotti | relevance check for Match |
commit | commitdiff | tree | snapshot |
2008-06-10 |
Enrico Tassi | initial qork for models |
commit | commitdiff | tree | snapshot |
2008-06-10 |
Wilmer Ricciotti | Added check of relevance lists for inductive types... |
commit | commitdiff | tree | snapshot |
2008-06-10 |
Enrico Tassi | lebesgue proved |
commit | commitdiff | tree | snapshot |
2008-06-10 |
Enrico Tassi | snapshot |
commit | commitdiff | tree | snapshot |
2008-06-09 |
Claudio Sacerdoti... | Most of the time, URIs can now be replaced with identif... |
commit | commitdiff | tree | snapshot |
2008-06-09 |
Claudio Sacerdoti... | It is now possible to use identifiers in place of URI... |
commit | commitdiff | tree | snapshot |
2008-06-09 |
Wilmer Ricciotti | Reverting to the previous version some files which... |
commit | commitdiff | tree | snapshot |
2008-06-09 |
Wilmer Ricciotti | more proof irrelevance |
commit | commitdiff | tree | snapshot |
2008-06-09 |
Enrico Tassi | initial work on lebesque |
commit | commitdiff | tree | snapshot |
2008-06-09 |
Enrico Tassi | exhaustivity completed |
commit | commitdiff | tree | snapshot |
2008-06-09 |
Enrico Tassi | exhaustivity, some work |
commit | commitdiff | tree | snapshot |
2008-06-08 |
Claudio Sacerdoti... | generalize no more required before elim |
commit | commitdiff | tree | snapshot |
2008-06-08 |
Claudio Sacerdoti... | generalize no more required before elim |
commit | commitdiff | tree | snapshot |
2008-06-08 |
Claudio Sacerdoti... | generalize no more required before elim |
commit | commitdiff | tree | snapshot |
2008-06-08 |
Claudio Sacerdoti... | generalize no more required before elim |
commit | commitdiff | tree | snapshot |
2008-06-08 |
Claudio Sacerdoti... | generalize no more required by elim |
commit | commitdiff | tree | snapshot |
2008-06-08 |
Claudio Sacerdoti... | Generalize no more required for elim. |
commit | commitdiff | tree | snapshot |
2008-06-08 |
Claudio Sacerdoti... | generalize no more required before elim |
commit | commitdiff | tree | snapshot |
2008-06-08 |
Claudio Sacerdoti... | generalize no more useful for elim |
commit | commitdiff | tree | snapshot |
2008-06-08 |
Claudio Sacerdoti... | Bug fixed: wrong default pattern for generalize. |
commit | commitdiff | tree | snapshot |
2008-06-08 |
Claudio Sacerdoti... | New: pattern for elim documented. |
commit | commitdiff | tree | snapshot |
2008-06-08 |
Claudio Sacerdoti... | Hypotheses patterns for elim implemented. No more need... |
commit | commitdiff | tree | snapshot |
next |