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

- 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.