refactoring ...

refactoring ...

cpr_cast closed! (after a bugfix in the "destruct" tactic)

1. nInversion/nDestruct ported to work with jmeq properly
2. axiom streicherK in logic.ma replaced with a computational proof
3. library changed accordingly

Debugging code commented out.

Ported changes amde on the main branch:
1. Reintroduced a failure cache
2. Corrected a bug in subsumption
3. Crippled the search space of not-last (side) equational goals.

- Reintroduction of a failure chache
-r
-e, and those below, will be ignored--

    ng_tactics/nnAuto.ml

Matitaweb: fixed bugs in commit.

commit by user utente3

commit by user utente2

Matitaweb: added a titlebar to the GUI.

Matitaweb: more changes to commit (now almost usable).

commit by user utente

Matitaweb: several improvements to svn interface.
Some cosmetic changes.

news update

typos ...

- first version of xhtbl
- first version of ld_basic_2.html (generated)

- new stylesheets for xhtml pages (ld_web)
- typo corrected in ld_web.css

Matitaweb: test commit.

Matitaweb: commit test.

Matitaweb: commit test.

Matitaweb: commit test.

commit by user andrea

Matitaweb: implementation of file-flagging for keeping track of modified files
proceeds.

new version

commit by user andrea

commit by user andrea

Matitaweb file flag test.

commit by user andrea

commit by user andrea

- xhtbl.css is ready!
- images ar now in a dedicated directory

Matitaweb: test commit.

Matitaweb: test commit.

Matitaweb: test commit.

Matitaweb: test commit.

Matitaweb: Library test.

...

Matitaweb: Some bugfixes concerning file flags.

Matitaweb:
1) Added experimental update functionality
2) Flagged library files -synchronized, modified, conflicted, unmanaged-
   (partial implementation)
3) Various cosmetic changes

still new colors ...

bugfix in one of the new colors :)

bugfix in remote update

new colors for the crux ...

Tutorial update.

Tutorial di Matita (lupo, capra, cavoli)

Not well understood patch: an assert false did occur, so I changed it to a
pattern matching failure. However, I do not know if this was due to a badly
defined notation or not.

- the confluence of context-senstitive parallel reduction (cpr) is closed!
- the theory of partial unfold on local environments (ltpss) is set up

Matitaweb: Fixed a bug which caused matita to forget the baseuri of the current
script when retracting to the top.

Map in NCicUtils now takes an optional boolea to disable head beta reduction.
We normalize cic terms in the paramodulation blob by stripping out names in
binders.

1) removed many debug prints
2) solved a bug in automation (we had forgotten to saturate clauses in
forward_infer_step, a mistake that prevented equations from being
indexed, resulting in almost certain failure of automation).
3) disabled alpha_eq in NCicBlob.compare, because it now requires a
status containing the correct environment, which can't be guessed
inside compare (enabling alpha_eq results in the automation
sporadically failing).

Matitaweb: disabled many verbose debug prints.

The Blob is not abstracted on the context any more.
The saturate function (that requires the environment now
contained in the status) is now external to the module.
It is defined in NCicBlob.
The functions mk_passive and mk_goals are now expecting
input terms already saturated.

some improvements about the partial unfold on terms (tpss)

Fixes a bug (introduced in the previous revision) which caused the environment
to forget its status.

This commit patches the environment and the library so that their status is
contained in the global status of Matita. This allows several users to execute
concurrently in the same instance of Matita, since they are now using
independent statuses.

File uploading

mah...

The tutorial on line.

The tutorial on line

unfold on terms completed!

remote update by make

added a pointer to helena in Wiedijk's list

update

Added debug print in NCicLibrary.serialize.

bug fix in xslt: missing ld namespace

refactoring completed!

commit by user utente1

bug fix in the dtd

refactoring and regeneration of lddl

the refactoring continues ...

refactoring ...

Matitaweb: layout change in the matitaweb inteface, in order to allow better
cross-browser compatibility.

- news update
- the download directory is now complete

- helm server url updated
- some renaming

initial commit of lambda_delta web site
(it was not maintained in svn so far)

- support for transitive closures started
- "unfold" component started
- we corrected one axiom of drop

Matitaweb: fixed "new file".

Matitaweb: New File functionality.

Matitaweb: Save as...

Matitaweb: makefile reverted to old (working) version.

Matitaweb: first attempt at "Save as".

Matitaweb: more changes to file selection dialog box.

Matitaweb: changes to file selection dialog box.

Matitaweb: changes to file selection dialog box.

Matitaweb: changes in file selection dialog box.

Matitaweb: Changes to the file selection dialog box.

Matitaweb: changes to file selection dialog box.

Matitaweb: Some changes in file selection dialogbox.

...

Changed behavior in matitaweb.js, function retrieveFile (it is now
compatible with Firefox, hopefully).

logic.ma is now enriched using the correct syntax.

Changed redirect behaviour of the daemon (incompatibility with browsers
different from google chrome).

- confluence of context-free reduction on terms (tpr) closed!
- substitution lemma for tpr closed!
- so-called "substitution lemma" closed!
- some annotating

When the user db is not found, matitaweb now creates a new one.

Removed ghost copy of a MatitaScriptLexer (moved from
components/content_pres/ to matita/)

First attempt at svn commit of developments.
Fixes a problem with hyperlinks (the </A> tag was not consumed correctly
if it appeared at the end of a command/tactic).

- the substitution lemma is proved!
- slight modification of parallel substitution and some renaming

commit by user utente

commit by user utente

- the theory of parallel substitution of local environments (ltps) is ready
- the theory of context-free parallel reduction of local environments (ltpr) is ready
- the proof of the substitution lemma for context-free parallel reduction is started ...
- some renaming and annotating