update in delayed_updating

+ mark label added
+ bugs fixed in depth and reduction
+ two notations changed

update in delayed_updating

+ a premise removed from lift_fsubst_sn
+ dfr and ifr restated to take equiprovability into account
+ notatation update for preterms

update in ground

+ advanced eliminators on lists

update in delayed_updating

+ commutation of lift and fsubst
+ preterms renamed as prototerms

update in grafite parser

+ parameter notation in record fields

update in ground

+ WIP on subsets

update in delayed_updating

+ proper condition for path
+ relation between lift and append proved

update in delayed updating

+ notation for "proper element"
+ bug fixed ub the notation of predicates

update in lib

+ notation for card decentralized

update in ground and delayed updating

+ notation at level 75 moved at level 70
+ dfr, ifr: path depth was not considered

update in delayed_updating

+ improved lift

update in delayed_updating

+ immediate reduction defined
+ some lemmas with lift simplified

update in delayed updating

+ some properties of lift

update in ground, static_2 and apps_2

+ updated notation for extensional equality

update in delayed_updating

+ updated notation for lists
+ WIP on lift

update in ground, basic_2A and apps_2

+ notation for lists: fixed and updated

update in ground

+ uniform total relocations

update in delayed updating

+ delayed focalized reduction

update in ground

+ composition for total relocation maps

Merge branch 'master' of ssh://matita.cs.unibo.it:/srv/git/helm

update in ground

+ positive application for total relocation maps completed

update in delayed_updating

+ terms are defined modulo logical equivalence

update in ground

+ basic support for subsets as predicates

update in delayed updating

+ WIP on dephi
+ some renaming
+ subset notation improved

update in delayed_updating

+ wip on predicate for bdd terms
+ updated notation
+ additions to lists

update in ground

+ updated notation and terminology for lists

update in ground

+ additions and corrections on lists

update in ground

+ advances on total redlocation

contribution on delayed updating begins

we place it here for convenience

update in ground

+ total relocation begins

Merge branch 'master' of ssh://matita.cs.unibo.it:/srv/git/helm

λδ web site update

+ updated bibliography

update in ground static_2 basic_2 apps_2

+ two sets of bold parentheses were used. now just one

update in ground

+ total relocation restarted

partial update in static_2

+ propagation of ground library in static_2/relocation begins
+ additions in ground

partial update in static_2

+ ground library propagated in static/syntax
+ additions in ground

partial update in static_2

+ propagating the ground library
+ one addition in ground

update in ground

+ minor bug fixed in a notation

partial commit in static_2

propagating the new ground library to static_2 begins

update in ground

+ one lemma was missing

update in ground

+ bug fixed in the notation of exp
+ minor bugs fixed

update in ground

+ some renaming

update in ground

+ new notation for head and tail

update in ground and static_2

+ notation update for tail function
+ predefined virtuals: one symbol added

update in alpha_1

+ type of terms redefined
+ Makefile added to lambdadelta/bin
+ a correction static_2/syntax/term.ma

λδ site update

+ one citation added to home page
+ one bug fixed in xhtbl.ml
+ ome comment added in gcp_cr.ma

update in ground

+ comments restyled

λδ site update

+ ground and documentation

probe

+ improved error handling

nCicLibrary

+ config flag added to emove old objects before storing new ones
  I don't even rememberwhy thisisnot done by default

update in ground

+ some renaming

cic notation parser

syntax of constructors updated to match syntax of definitions

milestone update in ground

+ generic relocation maps are now streams of booleans
+ some renaming and restyling
+ operator precedence more uniform
+ recomm updated for relocation

grafite parser updated

+ syntax for parameters added to constructors
  as it was done with definitions some time ago

propagating the arithmetics library, partial commit

+ relocation updated and ported (de Bruijn indexes now start at 1)
+ recomm updated to generate substitution files
+ results on positive integers added to arith
+ some corrections

update in ground

+ notation restyled

update in ground

+ xoa restyled
+ missing files committed

update in gruound

+ library refactored and restyled
+ recomm updated

update in ground

+ arith restyled
+ recomm updated

removing old contribs

+ RELATIONAL: side copies removed
+ developments.txt updated

removing old contribs

+ RELATIONAL
+ ONAG

propagating the arithmetics library, partial commit

+ counters (was: steps) ported and restyled
+ core notation: "pair" decentralized
+ some corrections and renaming

update in bin

+ new application "recomm"
  for restyling comments in λδ source files
+ minor corrections in ground and apps_2

propagating the arithmetics library, partial commit

+ lib ported
+ minor corrections and renaming
+ old parked version of ynat removed

milestone update in ground, partial commit

+ propagating the arithmetics library
+ gathering the arithmetics files
+ function composition respects extensional equivalence
+ minor corrections

arithmetics for λδ

+ arith.ma covered almost in full
+ minor additions and corrections

arithmetics for λδ

+ advances on maximum for non-negative integers
+ part of nat.ma used by λδ covered in full
+ minor additions and corrections

arithmetics for λδ

+ maximum for non-negative integers
+ minor corrections

arithmetics for λδ

strict order for non-ngative integers completed

arithmetics for λδ

+ subtraction for non-negative integers
+ web site update
+ apps_2/examples: minor update

arithmetics for λδ

+ predecessor for non-negative integers
+ web site update

arithmetics for λδ

we rebild the arithmetic library because lib/arithmetics/nat.ma has some problems:
- matitac does not compile it because of known time travel erropr
- too many indexed theorems make the search space explode during auto

λδ site update

+ old references to ground_2 removed
+ Makefile: bugfix

λδ-2B and λδ-ground repackaged for publication

+ web site update

λδ web site update

+ documentation updated

λδ site update

+ another Unicode character sponsored
+ Helena: minor updates
+ Ground: minor updates

update in static_2

one theorem renamed

update in basic_2

+ improved definition of fsb
+ some parked files removed

minor additions to standard library

....

milestone update in basic_2

+ improved rst-transition and related theory
+ minor improvements

update in static_2

+ generic equivalence generalizes syntactic equivalence and sort-irrelevant equivalence
+ minor corrections

decentralized notation in lambda

+ Makefile update

update in staic_2 and basic_2

+ an inversion lemma clarifies the link between rpx and req/reqx/lpx
+ some renaming

update in basic_2

+ rpx_req: cpx_teqx_conf_rex replaced by cpx_teqx_repl_reqx

milestone update in basic_2, update in ground and static_2

+ new definition of cpx and derivatives without the sort hierarchy parameter
+ sort hierarchy parameter removed from ex_fpbg_refl.ma

update in binararies for λδ

+ updated roles
+ some role specifications removed from basic_2A
+ updated web site

renaming in basics/relations

+ we rename adefinition that was clashing with λδ

update in standard library

+ some notations with ^ decentralized
+ one decentralized notation added to reverse_complexity/speedup.ma

ground_2 released and permanently renamed as ground

+ web site update
+ minor corrections

milestone update in ground_2 and basic_2A

+ basic_2A ported to ground_2
+ cpy, cpys and lsuby parked in basic_2A
+ ground_2 updated for basic_2A becomes an independent package
+ ground_2A removed
+ parked files for basic_2A moved in basic_2A
+ web site update

update in binaries for λδ

+ roles: multiple selection and expansion
+ roles: js updated to use multiple selection based on filter
+ roles: option -o
+ roles.osn: wip

update in binaries for λδ

+ roles: updated web interface with filter function in js

update in binaries for λδ

+ roles: updated status allows smarter semantics of option -a
+ roles: bug fixed in option -d
+ roles: improved web interface
+ roles: some typos fixed
+ roles.osn: wip

update in binaries for λδ

+ roles: options -d and -x
+ roles: improved web interface now is usable
+ roles.osn: additions through web interface started

update in binaries for λδ

roles: more transient information in the status
roles: refactored options -o -s -t to -t -n -s

update in binaries for λδ

+ roles: improved web interface
+ roles: -C option improved
+ roles: bug fixed in read_waiting
+ roles.osn regenerated correctly

update in binaries for λδ

roles: WIP ...

update in binaries for λδ

roles: initial infrastructure for the web interface

update in binaries for λδ

roles: options -m, -p and status file update

update in binaries for λδ

roles: option -o and status file update