web site updated with document J2

\lambda\delta version 2A released on Web site

- milestone update in basic_2 (basic_2a released)
- web site refactoring, update and bugfix

- the trace is explicit in all auto tactics with depth > 1
- one bug fixed
- the renaming continues ...

- some renaming according to the written version of basic_2
- more destructing lemmas invoked in place of buggy destructs

minor web site update

Typos.

- update in basic_2
- update of the web site: we added a "citations" section in the news

- grafiteParser: we added the comand "defined" as a presentational
alternative to "qed" for definitions.
- lambdadelta: we added an example about extended validity vs.
restricted validity + some minor corrections

more automation for cpcs ...

minor update in basic 2 and in the web site

update in basic_2 ...

- lambdadelta: minor corrections
- predefined_virtuals: some additions

we commit the web site again since last commit had some problems :(

old pabes removed

- update in basic_2
- web site major upddate

- some consequences of preservation added
- some renaming and some notation updated

catched typecheker failures in auto allow more applications of the tactic

contrib update ...

the commit was incomplete (as is often the case :( )

update in basic_2

- nnAuto: we catch TypeCheckerFailure generated at the end of
smart_apply (rel out of context) during equational reasoning,
and we treat it as an Error. TO BE UNDERSTTOD
(this TypeCheckerFailure dramatically interferes with automatic
proof search in \lambda\delta)
- lambdadelta: new definition of fpbg without fpbc + some refactoring

now the update is complete

previous commit was not complete :(

update in basic_2 ...

- fpbg can be reflexive (example given)
- so fpbu may use short steps rather than long steps
- some refactoring

minor update in basic_2 ...

notation update for pointwise union

big_O.ma

toolkit.ma

lablgtksourceview2 integrated into lablgtk2

minor update in basic_2 ...

notational change of lift, drop, and gget

update in basic_2 ...

slight refactoring in the proof of strong normalization

update in basic_2 ...

one more typo ...

bug fix in ththe notation for lists:
disambiguation of nil does not work very well in gcp_cr and gcp_aaa :(

...

...

added an example on lstas showing a difference with previous sta

- contrib update for version 2
- update in basic_2

New chapter on setoids.

chapter12 (coinductive) -> chapter13

milestone in basic_2 :)

commit completed! the new iterated static type assignment is up!

- the PARTIAL COMMIT continues, we issue the "reduction" component

- new stand-alone definition of lstas (sta and old lstas parked in etc)
- PARTIAL COMMIT: we issue just the components "static" and "unfold"

Notes.

A tentative chaptern on coinductive types.

Currently I hitted a major bug somewhere.

- update in basic_2
- minor update to the web site

some renaming and a minor addition

- bugfixed "aacr" allows to remove historical eta-conversions
  in the apparatus for strong normalization
- minor bugfixes in annotations
- xhtbl tables updated for the bugfixed stylesheets

- update in basic_2
- minor updates in the web site, including css bugfix

update in basic_2 ...

- some renaming and minor updates

- update in basic_2 and ground_2
- uodated web site

bugfix in source table :(

- basic_2: reaxiomatized snv with improved cpds and cpes simplifies preservation
- alpha_1: first commit
- ground_2/lib: one addition
- Makefile: improved contrib generation

new files

one property of abstract computation removed

refactoring of the butterflies :)

web site update

the generation of the web site is completed!

- update in ground_2 and basic_2
- the third page of the web site is generated

- irreflexivity of static type assignment iterated at least once
- some traces added for auto

- update in basic_2 and ground_2
- minor update of the web site

some renaming and some typos corrected ...

- xhtbl : support for named anchors (id's) and other improvements
- ld_web: additions for the "documentation" page

now the "news" page is generated

update for CamlP5

red butterfly added for version 1 :)

improved site map and version 2 page

- xhtbl: we added the real concatenation of cells (without added spaces)
- web site: we added a page for each version of \lambda\delta

named anchors replaced by ids as requested by xhtml

- xhtbl: support for relative links added
- web site: now the "forword" page is generated

minor update in basic_2

improved example: Delta must be a family of terms

- now unicode characters are counted :)
- now identifiers are counted as single characters

important update in basic_2: cpr is not antisymmetric

conjecture on antisymmetry of cpr finally closed
cpr is NOT antisymmetric: call-by-value beta-reduction takes two steps exactly

some additions and corrections ...

- we begin the new site based on ld_web
- xhtbl: xml namespaces and absolute atnl links are now supported
- lambdadelta_2 uploaded

- wrong version of drop was used in four places
- bugfixed css class in tables

update in basic_2

- ldrop is now drop as in basic_1
- notation change for tstc and leq

updated slides

pathologic @-typing removed by adding imp-introduction

misspelled filename :(

milestone reported on web site

- we upload communication #8
- update in basic_2 and ground_2

- some pending conjectures closed in basic_2 and ground_2
- bug fix in decidability of lift

milestone in basic_2 !!

milestone connit for preservation:
- for now we remove stratified equivalence for terms
  (it is much more complicated than expected)
- we park in etc a generalization of preservation

minor update in basic_2

- we introduce stratified term equivalence to remove the parameter g from cpx
- unused files removed from etc
- minor updates

update in basic_2 ...

reorganization of the "static" component:
from now on we use the non-stratified version of the static type assignment,
as in basic_1

preservation of stratified vaildity through ordinary reduction and static typing

update in basic_2 ...