long awaited update in basic_2

csx_lfsx eventually proved! (major result on lfsx)

update in basic_2

+ yet anothe equivalent of lfsx to be used in lfsx_pair_lpxs

update in basic_2

+ improved version of lfxs_trans_gen, now lfxs_trans_fsle
  based on an improved version of lexs_trans_gen
+ refactoring

update in basic_2

+ new equivalent of lfsx opens the road to lfsx_pair_lpxs
+ minor corrections

update in basic_2

+ new proof of cpx_frees_conf_lexs with fsle
+ refactoring

update in ground_2 and basic_2

+ minor additions
+ refactoring

advances on cpx_lfxs_conf_fle

+ transitivities for fle
+ minor additions

lref case closed in cpx_lfxs_conf_fle

+ premise with h.o equality added to the theorem

integrating the framework with fle ...

+ new ignores

two cases of cpx_lfxs_conf_fle closed

+ advances on fle
+ one inversion lemma missing in lveq
+ one character missing in predefined virtuals

xoa updated

a dependence from matita removed
optional generation of separated objects (this should be the default)

helena: updated prolog exportation to ld3 and ALT-0/PTS

update in basic_2

yet another definition of lveq allows to prove a missing lemma in lfxs_fle

update in ground_2 and basic_2

- new version of lveq completed: allows to prove all six main properties of fle, but lfxs_fle fails :(
- voids parked for now
- more ignores for the web site

\lambda\delta web site update for git

helena: warning removed and modifications for λΥP exportation

update in helena

- new system of attributes for terms
- exportation to λΥP λProlog engine
- now based on ocamlbuild

jet a change in dependences

work in progress with voids and lveq (was: the most recent voids)

update in ground_2 + \lambda\delta-related ignores

matita.basedir used consistently

more files to ignore

updated depend files

beginning of minimalist foundation from a student of Milly

Horrible workaround

Compiled with recent OCaml, Matita now fails removing
a notation when it starts. The patch avoids the assert
false. I have not investigated what's going on.

.depend{.opt} files changed

Patch to make it compile with recent OCaml

added .gitignore

OCaml special files ignored

patch to make it compile with recent OCaml versions

strange bug-fix to allow compilation on recent ocaml+camlp5o

Stupid fix to avoid new camlp5 bug with int64 literals

Patch to make it work with new versions of lablgtk2

- work in progress proceeds for the new definition of voids ...
- arith.ma: some additions and reordering

an addition for \lambda\delta

work in progress on a new definition of voids ...

the previous commit was incomplete :(

work in progress with fle ...

work in progress ...

- free variables innclusion (fle) encapsulates some complexity
  in the proof of a generalization of frees_lfxs_conf
- a refactoring solves a bug in dependences

update in basic_2

- equivalence between lfpxs and lpxs + lfeq proved
- more descriptions in basic_2_src.tbl

- lpx and lpxs restored to prove equivalene between lfpxs and lpxs + lfeq
- Makefile: number of objects and intrinsic loss factor added in summary for web page
- basic_2_src.tbl: more descriptions

update in basic_2 and in the corresponding web page

- equivalene of tc_lfxs and lex + lfeq proved
- bug fixed in fqu_lref_S

- ground_2: rtmap: disjointness relation
-           lib: some additions
- basic_2: first version of tc_lfxs_inv_lex_lfeq
           some improvements
           new explanatory column in basic_2_src.tbl

- dependences on ceq and ceq_ext fixed
- lfeq (was lleq) reintroduced
- some renaming

former commit completed: one file was missing :(

- ext2_tc added
- lexs_tc reconstructed
- support for lex (was lpx_sn) reintroduced
- fixed a bug about ceq

notational change in basic_2

- notation change for tdeq and related notions
- extra spaces removed in notation files
- bug fixed in replace.sh: the case of a wrong sed should be handeled correctly

update in basic_2

- lsubsx (replacement of lcosx) completed
- minor updates

- some proposition name clashes removed
- advances on lfsx_csx

advances on lfsx_csx ...

update in basic_2

lfsx_drops completed

update in basic_2 ...

- exclusion binder in local environments allows to complete lfsx_lfsx !
- advances on csx ...

update in basic_2

- exclusion binder in local environments
  the update is now complete, after bugs fixed in lfdeq.ma
- minor corrections

updated colors for summary tables in the web site

- cpxs completed
- changed colors in sunnary tables for web site

update in basic_2

- exclusion binder in local environments
  portions updated of: cpxs, lfpxs

update in basic_2 and apps_2

- exclusion binder in local environments
  component "rt_transition" completed by updating: fpb, fpbq
- one example file now works

update in basic_2

- exclusion binder in local  environments
  updated: cpm, cpr, lfpr, cpc
- some refactoeing and minor corrections

- update in basic_2
- "versions" table fixed in the web site

one file missing in previous commit :(

- exclusion binder in local environments:
  cpg, cpx, lfpx updated
- notation for lazyeq: fixes and additions

- one conjecture closed on lsubf
- some renaming in rtmap_sor

update in basic_2

- exclusion binder in local environments
  updating of component rt_transition started
  cpg completed

post milestone in basic_2

- exclusion binder in local environments
  component i_static updated
  (this is part of last milestone)

- milestone in basic_2
- update in ground_2

- exclusion binder added in local environments
  working components: syntax, relocation, s_transition, s_computation, static
- improved lsubf of which we hope to prove transitivity
- improvements in rtmap

update in basic_2

update in basic_2 due to previous update in grond_2

- web site update
- update in ground_2

- more results on relocation
- refactoring

notation bug due to previous refactoring

xoa notation refactoring and minor additions

one file was missing :(

more results on binders ...

extension of a relation to binders

component utf8_macros fully renamed

component syntax_extensions was not declared

more notation for s-steps

notation for clear

notational change for lexs

one file was missing :(

- more background for the exclusion binder
- some corrections

refactoring completed

refactoring ...

some improvements before setting up the exclusion binder

- notation for the exclusion binder in local envirinments
- advances on lfsx

- advances on lfpxs ...
- some instances of Conf3 discovered
- some refactoring

milestone in basic_2