- renaming completed!
- one more property of context-sensitive computation
- improved Makefile (from former commit)

We are decapitalizing the contributions' names ...

- update in Basic_2
- we added some information in thesunnary tables

- lambda_delta: morew propertie in context-sensitive computation
- formal_topology: compilation of categories.ma continues ...
- grafiteEngine.ml: coercions to sorts can now be defined with the short
syntax

Fixes bug where switching to a new tab the slider is not updated correctly.

commit by user andrea

commit by user andrea

commit by user andrea

commit by user utente2

commit by user ricciott

commit by user andrea

Axiom proved

Sectionin

commit by user utente2

commit by user andrea

more sections

small changes

Titols

Sections

commit by user andrea

commit by user utente2

section in chapter 2

commit by user andrea

Added sections in chapter 1.

Removed re.ma and re1.ma

commit by user andrea

commit by user andrea

commit by user andrea

commit by user andrea

commit by user utente2

commit by user ricciott

commit by user andrea

Forward compatibility with new releases of Camlp5.

Workaround for a BSD bug (submitted by Boender).

Bug fixed: horizontal scrolling now works correctly when the tab is changed.
The patch, however, is costly (everything is re-drawn twice).

MAJOR SPEED UP. The previous implementation of scrolling of the slidebar to
the end of the sequent was based on listening to signals. These signals:

1) were raised multiple times for each insertion (LOT of times!) making
   the scrolling extremely slow.
2) the callback was registered multiple times every time the user switched
   goal. This made the system slower and slower.

Minor speed up in the code.

commit by user andrea

Removed gif

chapter 9

Pictures

commit by user andrea

commit by user andrea

commit by user andrea

Small changes

Major speed-up improvement. Adding one callback per hyperlink was
extremely costly. It is now immediate.

chapter 9 and 10

commit by user andrea

- lambda_delta: "conversion" and "equivalence" components started
- formal_topology: porting to lib started. cprop_connectives compiles!

commit by user andrea

commit by user andrea

commit by user andrea

commit by user andrea

commit by user andrea

commit by user utente2

commit by user andrea

Splitted chapter 7

commit by user andrea

missing files in the former commit :(

commit by user andrea

commit by user andrea

commit by user andrea

commit by user andrea

commit by user andrea

commit by user andrea

commit by user andrea

commit by user andrea

commit by user andrea

commit by user andrea

commit by user andrea

commit by user andrea

commit by user utente2

commit by user andrea

some additions to Basic_2

- property S6 of stronfly normalizing terms proved
- more properties concerning context sensitive computation

site update

- we added a web page (Apps_2) for the checked applications of Basic_2
- we added some files to Basic_2
- we improved the Makefiles

- "functional" component moved to Apps_2
- property S5 of the candidates of reducibility almost proved ...

commit by user andrea

refiner porting from matita 1.

Integrations

Complete outline. Raw scripts.

- more properties on strongly normalizing terms ...

- site update

additions to Basic_2 ...

initial properies of the "same top term constructor" predicate

more results on strongly normalizing terms

additions to Basic_2

- more properties on strongly normalizing terms
- bugfix in Basic_1 annotations

additions to Basic_2

- strong normalization of abbreviation proved
- bug fix in the generation lemma for abbreviationof context=sensitive parallel reduction

- design table for Basic_2
- summary table for Basic_2 and Ground_2
- some additions to the Basic_2 file table
- some new cell styles for xhtbl
- syntax cor comments added to xhtbl
- some improvements in the Makefiles

- first properties of strongly normalizing terms
- contex-sensitive normal forms
- context-sensitive parallel computation of terms

- one file and three lemmas added to Basic 2
- bugfix in Makefile

- three lemmas on context sensitive parallel reduction closed

- notation fix for reducible and normal forms
- some refactoring
- improved Makefile produces a table with numerical summary

the Basic_2 page was not regenerated ...

we added summary and timeline to the Basic_2 page

Notation for destructuring let-in for triples fixed.

- transitivity of lenv refinement for atomic arity asignment proved! ...
- results on context-free normal forms refacored
- some annotation added