| 2010-09-28 |
Enrico Tassi | hints polished and fixed to allow recursive inference...
|
commit | commitdiff | tree |
| 2010-09-28 |
Enrico Tassi | nicer hints, 16.1->3 done
|
commit | commitdiff | tree |
| 2010-09-27 |
Enrico Tassi | many fixes to setoids for re, 16.1 almost done
|
commit | commitdiff | tree |
| 2010-09-27 |
Enrico Tassi | fixed notation for \cup and \cap
|
commit | commitdiff | tree |
| 2010-09-25 |
Enrico Tassi | some reorganization + some more re-setoids.ma proofs
|
commit | commitdiff | tree |
| 2010-09-23 |
Enrico Tassi | morphism support moved to sets/ and logic/cprop
|
commit | commitdiff | tree |
| 2010-09-23 |
Enrico Tassi | interpretation for <->
|
commit | commitdiff | tree |
| 2010-09-23 |
Enrico Tassi | fix typo
|
commit | commitdiff | tree |
| 2010-09-23 |
Enrico Tassi | patch by Brian committed, cut&paste should not crash...
|
commit | commitdiff | tree |
| 2010-09-23 |
Enrico Tassi | Setoid-Rewriting under Ex works for an arbitrary depth...
|
commit | commitdiff | tree |
| 2010-09-16 |
Enrico Tassi | fixed notation
|
commit | commitdiff | tree |
| 2010-09-12 |
Enrico Tassi | some more work
|
commit | commitdiff | tree |
| 2010-09-12 |
Enrico Tassi | Change (or better define) the order of hints premises.
|
commit | commitdiff | tree |
| 2010-09-12 |
Enrico Tassi | non uniform coercions landed in hints_declaration.ma...
|
commit | commitdiff | tree |
| 2010-09-09 |
Enrico Tassi | Some refactoring in set*.ma, some new notations and...
|
commit | commitdiff | tree |
| 2010-09-09 |
Enrico Tassi | th 16.2 proved in the setoids setting
|
commit | commitdiff | tree |
| 2010-09-08 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-09-08 |
Enrico Tassi | better not allowed sort elimination error messsage
|
commit | commitdiff | tree |
| 2010-09-08 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-09-08 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-09-08 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-07-29 |
Enrico Tassi | interpret non ambiguous symbols ASAP
|
commit | commitdiff | tree |
| 2010-07-28 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-07-28 |
Enrico Tassi | allows auto before eq is defined
|
commit | commitdiff | tree |
| 2010-07-22 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-07-22 |
Enrico Tassi | some work on \exists
|
commit | commitdiff | tree |
| 2010-07-22 |
Enrico Tassi | eq -> eq0 renaming
|
commit | commitdiff | tree |
| 2010-07-22 |
Enrico Tassi | useless box removed
|
commit | commitdiff | tree |
| 2010-07-22 |
Enrico Tassi | fixed precedence so that no () are needed around variable...
|
commit | commitdiff | tree |
| 2010-07-22 |
Enrico Tassi | do not apply hints if metaclosed
|
commit | commitdiff | tree |
| 2010-07-22 |
Enrico Tassi | avoid assert false, just fail generating the coercion
|
commit | commitdiff | tree |
| 2010-07-21 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-07-21 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-07-21 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-07-21 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-07-20 |
Enrico Tassi | completed lemma 17
|
commit | commitdiff | tree |
| 2010-07-19 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-07-15 |
Enrico Tassi | re 16.4 almost done
|
commit | commitdiff | tree |
| 2010-07-10 |
Enrico Tassi | big mess of notation
|
commit | commitdiff | tree |
| 2010-07-09 |
Enrico Tassi | more notation
|
commit | commitdiff | tree |
| 2010-07-07 |
Enrico Tassi | moved formal_topology into library"
|
commit | commitdiff | tree |
| 2010-07-06 |
Enrico Tassi | some notation for map_arrows2
|
commit | commitdiff | tree |
| 2010-07-01 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-06-30 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-06-30 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-06-30 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-06-30 |
Enrico Tassi | ....
|
commit | commitdiff | tree |
| 2010-06-29 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-06-29 |
Enrico Tassi | notation made half decent
|
commit | commitdiff | tree |
| 2010-06-28 |
Enrico Tassi | better notation for oalgebra
|
commit | commitdiff | tree |
| 2010-06-18 |
Enrico Tassi | ....
|
commit | commitdiff | tree |
| 2010-06-17 |
Enrico Tassi | off by one fixed
|
commit | commitdiff | tree |
| 2010-06-07 |
Enrico Tassi | some stuff on re
|
commit | commitdiff | tree |
| 2010-06-07 |
Enrico Tassi | unify left args of inductive types with left argus...
|
commit | commitdiff | tree |
| 2010-05-11 |
Enrico Tassi | little workaround for multiple screens, gdk support...
|
commit | commitdiff | tree |
| 2010-05-10 |
Enrico Tassi | new intro:
|
commit | commitdiff | tree |
| 2010-05-07 |
Enrico Tassi | trace generation with "// by _;"
|
commit | commitdiff | tree |
| 2010-05-07 |
Enrico Tassi | notation
|
commit | commitdiff | tree |
| 2010-04-15 |
Enrico Tassi | bool_ext on 'o' not on 'Prop' (they are convertible...
|
commit | commitdiff | tree |
| 2010-04-13 |
Enrico Tassi | fixed makefile
|
commit | commitdiff | tree |
| 2010-04-13 |
Enrico Tassi | auto destructs while introducing in the context
|
commit | commitdiff | tree |
| 2010-04-13 |
Enrico Tassi | print nobjects (hack with Obj.magic)
|
commit | commitdiff | tree |
| 2010-04-13 |
Enrico Tassi | catch the right exception, avoid uncaught Subst_not_found
|
commit | commitdiff | tree |
| 2010-04-13 |
Enrico Tassi | same heads different arity -> INCOMPARABLE
|
commit | commitdiff | tree |
| 2010-04-13 |
Enrico Tassi | some fixes to THF parser
|
commit | commitdiff | tree |
| 2010-04-13 |
Enrico Tassi | fixed support file for TPTP
|
commit | commitdiff | tree |
| 2010-04-08 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-04-08 |
Enrico Tassi | support axioms
|
commit | commitdiff | tree |
| 2010-04-08 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-04-08 |
Enrico Tassi | thf problems list for tptp 4.0.1
|
commit | commitdiff | tree |
| 2010-04-08 |
Enrico Tassi | fixed compiltion order of lexer/parser
|
commit | commitdiff | tree |
| 2010-04-08 |
Enrico Tassi | THF parser received some care
|
commit | commitdiff | tree |
| 2010-04-07 |
Enrico Tassi | THF parser for TPTP
|
commit | commitdiff | tree |
| 2010-03-02 |
Enrico Tassi | Constants are indexed using the Reference, not the...
|
commit | commitdiff | tree |
| 2010-02-11 |
Enrico Tassi | minimal sequent height set to 1
|
commit | commitdiff | tree |
| 2010-02-11 |
Enrico Tassi | some experiment filtering with height
|
commit | commitdiff | tree |
| 2010-01-07 |
Enrico Tassi | ....
|
commit | commitdiff | tree |
| 2010-01-07 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-01-07 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-12-30 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-12-01 |
Enrico Tassi | porting to lablgtk2 >= 2.14 and releasing
|
commit | commitdiff | tree |
| 2009-12-01 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-10-30 |
Enrico Tassi | auto snapshot
|
commit | commitdiff | tree |
| 2009-10-28 |
Enrico Tassi | better indentation
|
commit | commitdiff | tree |
| 2009-10-28 |
Enrico Tassi | better indentation
|
commit | commitdiff | tree |
| 2009-10-28 |
Enrico Tassi | better comments and indentation
|
commit | commitdiff | tree |
| 2009-10-28 |
Enrico Tassi | use prop_only to filter instead of repeting the same...
|
commit | commitdiff | tree |
| 2009-10-28 |
Enrico Tassi | better logging
|
commit | commitdiff | tree |
| 2009-10-28 |
Enrico Tassi | better logging and immediate pruning of new goals when
|
commit | commitdiff | tree |
| 2009-10-28 |
Enrico Tassi | auto navigates a real tree, not a flattened one
|
commit | commitdiff | tree |
| 2009-10-28 |
Enrico Tassi | labels in group_by_tac
|
commit | commitdiff | tree |
| 2009-10-28 |
Enrico Tassi | new data structures for auto
|
commit | commitdiff | tree |
| 2009-10-28 |
Enrico Tassi | do not put " around node name, otherwise names like...
|
commit | commitdiff | tree |
| 2009-10-28 |
Enrico Tassi | export group_by_tac
|
commit | commitdiff | tree |
| 2009-10-23 |
Enrico Tassi | added code to print the tree
|
commit | commitdiff | tree |
| 2009-10-23 |
Enrico Tassi | CSC proof made by paramod
|
commit | commitdiff | tree |
| 2009-10-23 |
Enrico Tassi | more functions
|
commit | commitdiff | tree |
| 2009-10-22 |
Enrico Tassi | new instantiate, only known bug is w.r.t. in/out scope...
|
commit | commitdiff | tree |
| 2009-10-22 |
Enrico Tassi | the trie indexes terms up to 10 nested applications...
|
commit | commitdiff | tree |
| 2009-10-22 |
Enrico Tassi | more auto
|
commit | commitdiff | tree |
| next |
projects / helm.git / search