2002-12-04 |
natile | *** empty log message *** |
tree | commitdiff |
2002-12-04 |
Claudio Sacerdoti... | New feature: the user can now enter the list of "must... |
tree | commitdiff |
2002-12-04 |
Claudio Sacerdoti... | * mQueryLevels interface clean-up |
tree | commitdiff |
2002-12-04 |
Claudio Sacerdoti... | Simplification euristic improved. |
tree | commitdiff |
2002-12-04 |
Claudio Sacerdoti... | New tactic fold_simpl. |
tree | commitdiff |
2002-12-04 |
Claudio Sacerdoti... | * fold_tac has now a new parameter, which is the reduct... |
tree | commitdiff |
2002-12-03 |
Claudio Sacerdoti... | Typing of intros_tac improved. It now has a parameter... |
tree | commitdiff |
2002-12-03 |
Claudio Sacerdoti... | First working version of the possibility to introduce... |
tree | commitdiff |
2002-12-03 |
Michele Galatà | Added new tactics: Exists, Split, Assumption, Absurd... |
tree | commitdiff |
2002-12-02 |
Claudio Sacerdoti... | First implementation of the new generalized SearchPatte... |
tree | commitdiff |
2002-12-01 |
Enrico Tassi | - now esempi/fourier/ is he dir for all fourier extras |
tree | commitdiff |
2002-11-29 |
natile | Now MQueryGenerator generates the query and MQueryLevel... |
tree | commitdiff |
2002-11-29 |
Enrico Tassi | bug in hypotesis parsing solved |
tree | commitdiff |
2002-11-27 |
Claudio Sacerdoti... | * The new query language (now broken) works only on... |
tree | commitdiff |
2002-11-27 |
Ferruccio Guidi | generator patched |
tree | commitdiff |
2002-11-26 |
Enrico Tassi | comments in fourier.ml now are in ocamldoc style |
tree | commitdiff |
2002-11-26 |
Ferruccio Guidi | New module for level management (was in MQueryGenerator) |
tree | commitdiff |
2002-11-26 |
Ferruccio Guidi | Generator updated for new MathQL.ml |
tree | commitdiff |
2002-11-22 |
natile | toplevel.ml patched but it doesn't compile with open... |
tree | commitdiff |
2002-11-21 |
Claudio Sacerdoti... | WARNING!!! |
tree | commitdiff |
2002-11-20 |
Enrico Tassi | - removed: cut_tac False to demostrate False |
tree | commitdiff |
2002-11-19 |
Claudio Sacerdoti... | ~ask_dtd_to_the_getter parameter added to Cic2Xml.print... |
tree | commitdiff |
2002-11-19 |
Claudio Sacerdoti... | Param ~ask_dtd_to_the_getter added to Cic2Xml.print_object. |
tree | commitdiff |
2002-11-19 |
Claudio Sacerdoti... | Big change: Qed saves the theorem/definition and regist... |
tree | commitdiff |
2002-11-18 |
Claudio Sacerdoti... | Interface improvement (???): the Check button has been... |
tree | commitdiff |
2002-11-18 |
Claudio Sacerdoti... | Small interface improvement: the menu is now in an... |
tree | commitdiff |
2002-11-18 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
2002-11-18 |
Claudio Sacerdoti... | Interface improvement: |
tree | commitdiff |
2002-11-18 |
Claudio Sacerdoti... | Code clean-up: the widget in the lower-left corner... |
tree | commitdiff |
2002-11-18 |
Claudio Sacerdoti... | Aliases definition removed from the CIC textual parser. |
tree | commitdiff |
2002-11-18 |
Claudio Sacerdoti... | Inteface improvement: the "Edit Aliases..." menu entry... |
tree | commitdiff |
2002-11-18 |
Claudio Sacerdoti... | Major interface improvements. |
tree | commitdiff |
2002-11-18 |
Claudio Sacerdoti... | Rendering of InductiveDefinitions, Variables and Axioms... |
tree | commitdiff |
2002-11-15 |
Claudio Sacerdoti... | Order of the generated metavariables for apply fixed... |
tree | commitdiff |
2002-11-15 |
Claudio Sacerdoti... | Bug fixed: conjectures were printed in the wrong order. |
tree | commitdiff |
2002-11-15 |
Claudio Sacerdoti... | * Bug fixed: a real empty page is now really used for... |
tree | commitdiff |
2002-11-15 |
Claudio Sacerdoti... | Residual interface bug fixes: no sequent page is now... |
tree | commitdiff |
2002-11-15 |
Claudio Sacerdoti... | Small interface improvement: the first goal page is... |
tree | commitdiff |
2002-11-15 |
Claudio Sacerdoti... | Small interface improvements. |
tree | commitdiff |
2002-11-14 |
Claudio Sacerdoti... | Other small improvements to the general window layout. |
tree | commitdiff |
2002-11-14 |
Claudio Sacerdoti... | Small interface improvement: selecting something in... |
tree | commitdiff |
2002-11-14 |
Claudio Sacerdoti... | Interface improvement: |
tree | commitdiff |
2002-11-13 |
Claudio Sacerdoti... | Interface improvements: the window to disambiguate... |
tree | commitdiff |
2002-11-12 |
Claudio Sacerdoti... | A frame now surrounds the XMHTML widget. |
tree | commitdiff |
2002-11-12 |
Claudio Sacerdoti... | Heavy restyling of the interface. |
tree | commitdiff |
2002-11-11 |
Enrico Tassi | An old bug in 'eqT' hipotesys solved |
tree | commitdiff |
2002-11-06 |
Claudio Sacerdoti... | - big interface changes: open goals are now collected... |
tree | commitdiff |
2002-11-04 |
Claudio Sacerdoti... | nameObject ==> objectName |
tree | commitdiff |
2002-11-04 |
Claudio Sacerdoti... | The reduction tactics are now shared between ReductionT... |
tree | commitdiff |
2002-11-04 |
Claudio Sacerdoti... | The fold tactic of proofEngine now uses ReductionTactic... |
tree | commitdiff |
2002-11-04 |
Claudio Sacerdoti... | - Comments updated |
tree | commitdiff |
2002-11-04 |
Claudio Sacerdoti... | - synchronization with the main branch |
tree | commitdiff |
2002-11-04 |
Claudio Sacerdoti... | - porting to the new theory with explicit named substit... |
tree | commitdiff |
2002-11-04 |
Claudio Sacerdoti... | - new fold tactic |
tree | commitdiff |
2002-11-04 |
Claudio Sacerdoti... | - new CicTextualParser |
tree | commitdiff |
2002-10-31 |
Claudio Sacerdoti... | Several bug-fixes: |
tree | commitdiff |
2002-10-31 |
Claudio Sacerdoti... | Bug fixed: the declared number of new goals of Apply... |
tree | commitdiff |
2002-10-31 |
Claudio Sacerdoti... | Better layout of the buttons. |
tree | commitdiff |
2002-10-31 |
Michele Galatà | Added variousTactic with Constructor, Left, Right,... |
tree | commitdiff |
2002-10-31 |
Claudio Sacerdoti... | - ElimIntrosSimpl now implemented using tacticals.... |
tree | commitdiff |
2002-10-31 |
Claudio Sacerdoti... | explicit namd substitutions introduced |
tree | commitdiff |
2002-10-30 |
Claudio Sacerdoti... | Undo of the previous commit (that was a mistake). |
tree | commitdiff |
2002-10-30 |
Claudio Sacerdoti... | Bug fixed in reduction/simplification of explicit named... |
tree | commitdiff |
2002-10-30 |
Claudio Sacerdoti... | Dead code removal. |
tree | commitdiff |
2002-10-30 |
Claudio Sacerdoti... | Minor interface improvement. |
tree | commitdiff |
2002-10-30 |
Claudio Sacerdoti... | - (Partial) porting to the new theory with explicit... |
tree | commitdiff |
2002-10-25 |
no author | This commit was manufactured by cvs2svn to create branch |
tree | commitdiff |
2002-10-09 |
no author | This commit was manufactured by cvs2svn to create branch |
tree | commitdiff |
2002-10-02 |
Enrico Tassi | tactic update |
tree | commitdiff |
2002-09-27 |
Claudio Sacerdoti... | Better handling of queries. Now both the locate and... |
tree | commitdiff |
2002-09-20 |
Claudio Sacerdoti... | change code moved to change_tac (functional version... |
tree | commitdiff |
2002-09-19 |
Enrico Tassi | Tactic update |
tree | commitdiff |
2002-09-18 |
Claudio Sacerdoti... | Small code improvement. |
tree | commitdiff |
2002-09-18 |
Enrico Tassi | Tactic update |
tree | commitdiff |
2002-09-17 |
Ferruccio Guidi | new query generator |
tree | commitdiff |
2002-09-16 |
Claudio Sacerdoti... | List of tactics implemented and to implement (italian... |
tree | commitdiff |
2002-09-13 |
Ferruccio Guidi | restricted mode to use when the database is down :) |
tree | commitdiff |
2002-09-13 |
Ferruccio Guidi | query generator timing feature improved |
tree | commitdiff |
2002-09-13 |
Claudio Sacerdoti... | ring.ml* splitted into ring.ml* and tacticals.ml* |
tree | commitdiff |
2002-09-13 |
Claudio Sacerdoti... | then_ tactical implemented (equivalent to the tclTHEN... |
tree | commitdiff |
2002-09-13 |
Enrico Tassi | Fourier tactic update |
tree | commitdiff |
2002-09-09 |
Claudio Sacerdoti... | When locate is used during the lexing phase, it may... |
tree | commitdiff |
2002-09-09 |
Claudio Sacerdoti... | Patch applied to the locate query: when used to retriev... |
tree | commitdiff |
2002-09-09 |
Enrico Tassi | Fourier tactic update |
tree | commitdiff |
2002-09-07 |
Enrico Tassi | First works |
tree | commitdiff |
2002-09-05 |
Ferruccio Guidi | mQueryGenerator and topLevel patched |
tree | commitdiff |
2002-09-05 |
Ferruccio Guidi | some small improvements: command line sintax changed... |
tree | commitdiff |
2002-09-04 |
Claudio Sacerdoti... | The parser (the lexer indeed) now use the locate query... |
tree | commitdiff |
2002-09-04 |
Enrico Tassi | Fourier tactic |
tree | commitdiff |
2002-08-29 |
Michele Galatà | Type expression simplified. |
tree | commitdiff |
2002-08-29 |
Michele Galatà | Comment typo fixed. |
tree | commitdiff |
2002-08-27 |
Claudio Sacerdoti... | Interface file created. Missing from previous commit. |
tree | commitdiff |
2002-07-29 |
Claudio Sacerdoti... | Updated to use the new parser that creates (stacks... |
tree | commitdiff |
2002-07-22 |
Claudio Sacerdoti... | Many improvements in tactics (and tactical) representation: |
tree | commitdiff |
2002-07-02 |
Stefano Zacchiroli | Added examples. |
tree | commitdiff |
2002-07-02 |
Stefano Zacchiroli | bugfix: Ring will work again with varmaps :-) |
tree | commitdiff |
2002-07-01 |
Stefano Zacchiroli | - added Ring tactic on reals |
tree | commitdiff |
2002-07-01 |
Stefano Zacchiroli | bugfix that inhibit the removal of certain hypotheses |
tree | commitdiff |
2002-07-01 |
Stefano Zacchiroli | bug fix: handled LetIn case in simpl |
tree | commitdiff |
2002-07-01 |
Ferruccio Guidi | mathQL modified, stderr corrected to stdout im mathql_i... |
tree | commitdiff |
next |