basic_2: stronger supclosure allows better inversion lemmas
ground_2: more results on sle and sor (rtmap)

some improvements towards the confluence of lfpr ...

milestone in basic_2!

one file was missing :(

diamond property of reduction!

first results on lfpr as a base for the diamond property ...

update in basic_2 ...

more results on cpm ...

one more paper citing \lambda\delta

update in ground_2 and basic_2

bug fix in the context reduction rule for cast (cpm)

we count rt parallel steps in a different way:
we use the maximum, that is idempotent, rather than the sum

xhtml simplified

more corrections to xhtml

corrected xhtml

site update

- initial page for osn ...
- some bug fixed

basic properties of cpr ...

- matex: notational macros for 0-ary constants
- stylesheets and Makefiles: minor improvements

- matex: we separate axioms (propositions) and assumptions (other)
- matex.sty: some improvements including
                  color for metalinguistic term constructions
- stylesheets: some improvements including more notation for basic_1

first definition of cpm:
the contextual rule for cast is incorrect :(

update in basic_2 ...

lfpx_drops completed!

totality of co-composition !

more notation for basic_1 ...

- matex: minor improvements
- latex stylesheets: more notation for basic_1
  now we use just the stix fonts

updating the dropable-related definitions with coafter ...

corrections to use less font packages (TeX was complaining)

- matex: minor corrections to handle applications with many arguments
- matex test stylesheets: some improvements, notation for ground_1 completed

does_not_occur documented

- improved support for case
- support for renaming constants

update in ground_2 and basic_2

frees_drops completed!

work in progress on frees_drops

MaTeX:
- notational macros for constants
- notational macro for quantification of propositions
matex.sty:
- support for math mode
- improved rendering of basic constructions
test style sheets
- some notational macros for legacy_1

- source web pages for lambdadelta_1
- minor bugs fixed in the web site

- update in ground_2 and basic_2
- updated documentation

frees_drops, initial versrion

some results on co-composition ...

more results on sor ...

initial support for lfpx_drops ...

more files missing :((

une file was missing :(

bug fixing ...

initial support for lfpx (replaces lpx and the parked llpx)

added config.ac to the tarball for debian packages

Was it really required? I don't know but it worked like that before.

initial support for LaTeX-defined notatopn

- support fof global alpha-conversion with hyperlinks
- Makefile: a bug fixed

update in basic_2

- notational change for cpg and cpx
- versions table updated on site

update in basic_2

- first results on cpx (dericed from those on cpg)
- minor bugs fixed

update in ground_2 and basic_2

bug fix in cpg allows to prove lsubr_cpg_trans

- ground_2: support for lifts_div4
- basic_2: cpg_drops competed

news for matita 0.99.3

the source code of matita 0.99.3 is online

bugfix ind docbook code for the relise of matita 0.99.3

some renaming and reordering of variables
the commit works up tp the "static" component + lpg.ma

pre commit for matita version 0.99.3

- matex: support for alpha-conversion completed
- matex.sty: hyperlinks without labels
- registry: support or triples

exportation of lambdadelta 1 with flavoured let recs

- partial commit of rt_transition  ...
- renaming in equivalence, dynamic, examples

milestone in basic_2 ...

ground_2: generic rt-transition counter

As required by M. Maietti,
cyclic sort hierarchies are now allowed through the "cyclic" keyword
so we can write:
universe cyclic constraint Type[U] < Type[U].
definition inconsistent: Type[U] ≝ Type[U].
matitaclean all is required after this commit

refactoring to park the notions:
lstas, unfold, crr, cir, cnr, crx, cix, cnx

universary milestone in basic_2

- former llpx_sn an lleq reactivated as lfxs and lfeq

- first working commit of the static component ..
- updates on some web pages

- advances on drops
- partial commit of the "static" component

renaming ...

minor additions :)

update in ground_2 and basic_2

- commit of the "s_computation" component ...
- additions in ground_2/relocation
- milestonee added in basic_2
- minor corrections

the newly generated web pages ...

- advances in the site generation architecture
- more on OSN and on the disclaimer

one file was missing

EBNF definition of OSN begins ...

- initial description of OSN
- ld_web: minor updates

images for Open Symbolic Notation (OSN)

update in ground_2 and basic_2 ...

- new component "s_transition" for the restored fqu and fquq
- minor additions
- notation update
- partial commit in the "static" component to park da and lsubd

- uniform relocations
- more results on at and after

minor correction on "source" production

minor additions ...

update in basic_2 and apps_2 ...

- minor corrections
- web pages for nasoc_2 and apps_2 are up again

another file was missing :(

- probe: now includes source character count (was: mac)
- lambdadelta: summaries are generated using the updated probe

support for printing the number of objects grouped by flavour

more files to commit .... :(

- ng_kernel: we print the offending term when guarded_by_constructors fails
- probe: we print the roots when more than one root is found
- lambdadelta: first working commit for the "relocation" component

update in ground_2

rtmaps with finite colength

advances in the theory of drops, lexs, and frees ...

- new syntax for let rec/corec with flavor specifier (tested on lambdadelta/ground_2/)
- source specifier on inductive/coinductive types (implies matitaclan all)
- minor additions

- ground_2: some additions
- basic_2/grammar: added missing files

partial commit in the relocation component to move some files ...

more results on after ...