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

- we shared the atomic term constructions
- we fixed the notation of the binary term construction
- we inverted the dependences of cl_shift and cl_weight

- the shift function is now defined and cpr_shift_fwd is proved
- tentative definition of the structures for the wh normal forms
- definition of lists without the [...] notation
- some refactoring and annotating (we separate lemmas from facts)

- weakening leq, we proved cpr_bind_dx
- we imple,ented some statistics in the Makefile

one reduction rule (tpr) was redundant

- confluence of parallel substitution (tps) closed! (a bug in an
inversion lemma was in the way)
- some refactoring

we now use non-telescopic substitution in parallel reduction, rather
than the telescopic one. This choice weakens the step of
context-sensitive reduction a bit while maintaining the expected
properties

- tentative definition of lcpr (contex-sensitive parallel reduction on
local environments)
- some refactoring

the refactoring was not really complete

refactoring completed

- some refactoring
- we fixed some wrong preambles in the scripts

- matitaclean greatly improved but ...
...  LibraryClean.clean_baseuris is not implemented yet :D

refactoring completed!

the refactoring continues ...

the refactoring continues ...

lambda-delta must be a contrib

lambda-delta must be a contrib

some refactoring

confluence of parallel substitution (tps) started ...

- tps_tpr closed! (substitution is a reduction)
- some refactoring

- cpr is now defined and the cpr_flat propery is proved! (it did not
hold in the first version of the calculus because cpr (aka pr2) was
badly designed).
- relocation properties of tpr closed!
- fixed bug in drop (base case was too restrictive)
- some refactoring

- transitivity of parallel telescopic substitution closed!
- some refactoring

the generation of the multiple conjunction is now supported!

confluence of tpr completed!

confluence: case 13 closed

xoa: new binary for the generation of multiple logical constants
lambda-delta: integration with xoa and a lemma about a xoa constant

- xoa: bug fix and improvement
- *_defs: optimization
- confluence: case "flat-theta" closed

tpr: more inversion lemmas and a main property stated

lift_weight: bug fix

- inversion lemmas for tpr completed!
- bug fix in lpr interpretation

- some renaming
- first third of confluence (tpr) closed

- sone refactoring
- notation fix
- telescopic substitution replaced by parallel substitution
- context-free parallel reduction added

confluence of reduction started ...

one main propery of drop closed, one added

two more main properties of drop closed

Matitaweb: fixed a bug concerning matita/html/xml escaping, which showed when
retrieving some nasty scripts from the server.

1) Matitaweb now disambiguates scripts as it runs them

2) Fixed bugs in HTML escaping (also changed the syntax of annotations in
   matita scripts)

first main property of drop closed

- drop_main: bug fix
- pr_lift: closed!

- nnAuto.ml: width overflows are warnings, not errors
- matitaScript.ml: backup source file with ~ reactivated
- lambda-delta: main properies of lift closed!

one main property of lift closed

- functional properties of lift closed!
- the proof of a main property of lift was lost due to a segmentation
fault of auto :-((

more lemmas and some generated logical constants for them

The name of the constructor for jmeq changed.

Bug fixed: when we try to add an object and it is not _directly_ well typed
(i.e. it is not well typed, and not because it depends on a non-well-typed
object in the library), we should not remember it, since the user can change
the definition and try again.

Use replace when switching tabs (see previous commit).

New function replace to be used in place of time_travel every time the user
switches to a new tab. In this way, every tab is independent and it only sees
the objects defined in that tab. This fixes the following bug: in tab A go
down; go down in tab B; go up in tab A (at this point also the objects declared
in B where removed); do something in B or go up in B (BOOM))

Dead code removed from the interface. It is used internally via references.

Changes to TeX-macro conversion.

Matitaweb: Bugfix for TeX-macro conversion.

Matitaweb: changes to utf8MacroTable.js

Matitaweb: changes to utf8MacroTable.js.

Matitaweb: TeX-like macro handling.

Changes to utf8MacroTable.js.

Added Utf8MacroTable for MatitaWeb.

More keyboard handling tests

- new definition of subst based on drop
- pr is now based on drop

more tests on keyboard handling.

more tests on keyboard events.

more tests on keyboard events.

more keyboard events tests.

more keyboard events tests.

more keyboard events tests.

more keyboard tests.

more keyboard events tests

more keyboard event tests

more tests with keyboard events.

minor bugfix

Testing keyboard events handling.

long file names caused indentation underflow (String.make) when times
were displayed

- some depend files
- bug fix in grafiteAstPp.ml
- some assertions in matitaEngine.ml