| 2009-05-25 |
Enrico Tassi | nasty change in the lexer/parser: |
tree | commitdiff |
| 2009-04-30 |
Enrico Tassi | run check_if_goal_is_solved on all goals (active+passive) |
tree | commitdiff |
| 2009-04-28 |
Enrico Tassi | huge commit in automation: |
tree | commitdiff |
| 2009-04-22 |
Enrico Tassi | demodulate takes an extra argument 'all', if present... |
tree | commitdiff |
| 2009-04-21 |
Ferruccio Guidi | - MatitaMisc: we factorized here the function out_pream... |
tree | commitdiff |
| 2009-04-21 |
Enrico Tassi | fixed last file restricting auto tables |
tree | commitdiff |
| 2009-04-20 |
Enrico Tassi | - init_cache_and_tables rewritten using the automation_... |
tree | commitdiff |
| 2009-04-15 |
Ferruccio Guidi | - transcript: bugfix |
tree | commitdiff |
| 2008-11-15 |
Enrico Tassi | rules fixed |
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-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-04 |
Enrico Tassi | fixed notation |
tree | commitdiff |
| 2008-09-04 |
Enrico Tassi | restored |
tree | commitdiff |
| 2008-09-04 |
Enrico Tassi | removed old non-working file |
tree | commitdiff |
| 2008-08-27 |
Claudio Sacerdoti... | Convergence is now defined. |
tree | commitdiff |
| 2008-08-25 |
Claudio Sacerdoti... | New cool "type-checking" notation using colors 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-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 |
| 2008-07-15 |
Enrico Tassi | more notation moved to core notation, unification of... |
tree | commitdiff |
| 2008-07-11 |
Claudio Sacerdoti... | A very nice experiment using notation: we define the... |
tree | commitdiff |
| 2008-07-09 |
Enrico Tassi | better notation |
tree | commitdiff |
| 2008-07-09 |
Enrico Tassi | minor fixes |
tree | commitdiff |
| 2008-07-09 |
Enrico Tassi | CProp hierarchy fixed: |
tree | commitdiff |
| 2008-07-04 |
Claudio Sacerdoti... | More definitions, following Ciraulo's Phd Thesis "Const... |
tree | commitdiff |
| 2008-07-04 |
Claudio Sacerdoti... | Compatibility finished. |
tree | commitdiff |
| 2008-07-04 |
Claudio Sacerdoti... | Nice: cotransitivity proved. |
tree | commitdiff |
| 2008-07-03 |
Claudio Sacerdoti... | More work. |
tree | commitdiff |
| 2008-07-03 |
Claudio Sacerdoti... | First few lemmas. But I have some problems in making... |
tree | commitdiff |
| 2008-07-03 |
Claudio Sacerdoti... | First experiment in Padua about formal topologies. |
tree | commitdiff |
| 2008-06-24 |
Enrico Tassi | notation factored, coercion commant taking terms and... |
tree | commitdiff |
| 2008-06-19 |
Enrico Tassi | notation on steroids: 'term 40 x' is a valid variable... |
tree | commitdiff |
| 2008-06-09 |
Claudio Sacerdoti... | Most of the time, URIs can now be replaced with identif... |
tree | commitdiff |
| 2008-06-08 |
Claudio Sacerdoti... | generalize no more required before elim |
tree | commitdiff |
| 2008-05-26 |
Enrico Tassi | new, more rigid syntax, for auto_params affecting the... |
tree | commitdiff |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
tree | commitdiff |
| 2008-04-08 |
Enrico Tassi | added simplify to avoid ugly proofterm |
tree | commitdiff |
| 2008-03-20 |
Claudio Sacerdoti... | Script fixed (it did not compile due to a mistake befor... |
tree | commitdiff |
| 2008-03-20 |
Enrico Tassi | changed auto_tac params type and all derivate tactics... |
tree | commitdiff |
| 2008-02-08 |
Claudio Sacerdoti... | A formalization of modified realisability with truth... |
tree | commitdiff |
| 2008-01-11 |
Enrico Tassi | increased timout |
tree | commitdiff |
| 2008-01-11 |
Enrico Tassi | increased a timeout, matitac (not .opt) should be able... |
tree | commitdiff |
| 2007-11-12 |
Ferruccio Guidi | - destruct tactic: automatic simplification in case... |
tree | commitdiff |
| 2007-10-28 |
Claudio Sacerdoti... | Nil => nil; Cons => cons |
tree | commitdiff |
| 2007-10-14 |
Claudio Sacerdoti... | Caseness problems fixed. |
tree | commitdiff |
| 2007-10-14 |
Claudio Sacerdoti... | Some lemmas moves to the file they belong to. |
tree | commitdiff |
| 2007-08-28 |
Claudio Sacerdoti... | * definition of implication free propositional formulas |
tree | commitdiff |
| 2007-05-24 |
Enrico Tassi | auto and autogui... some work |
tree | commitdiff |
| 2007-05-17 |
Enrico Tassi | auto rewritten with only one tail recursive function. |
tree | commitdiff |
| 2006-12-06 |
Claudio Sacerdoti... | More simplification using better notation. |
tree | commitdiff |
| 2006-11-30 |
Claudio Sacerdoti... | Notation \middot used everywhere in place of *. |
tree | commitdiff |
| 2006-11-30 |
Claudio Sacerdoti... | I have changed the nice notation for derivatives a... |
tree | commitdiff |
| 2006-11-30 |
Claudio Sacerdoti... | Added a demo for Matita: two slightly different proofs... |
tree | commitdiff |
|
projects / helm.git / history