some more work to factorize out uninteresting parts of the proof...
still to close the key lemma...

more work to try to understand where the issue is

lost in the wood

more work

few more steps

more work

some more work

more work on q

some more work

better, reparsable, notation

removed <_,_> notation second interpretation for dependent pair, since it used
to have an exponential slowdown on refinement of huge terms....

notation factored, coercion commant taking terms and not only URI

missing file added

metaAut.xlate_item started

we set the http daemon timeout to 15 minutes, which is the default timeout of   wget, because some proof terms are processed in more than 5 minutes.

more work, but russell too slow

add \\ in front of tex macros

notation support fixed to parentesize in a more sane way and
andded two windows:
1) tex/utf8 table
2) terms grammar

stylesheet application moved after header send

xxx

- grafiteParser.ml: the callback invocation was displaced
- cicNotationPres.ml: hack to have more brackets because
  (forall .. \to ..) was rendered without brackets. FIXME!
- LAMBDA-TYPES: improved Makefile

left -> right

Fixed bugs in the documentation of notation.
All TODOs left I do not know how to fill.

More documentation for notation.

Further documentation for notation.

- partial implementation of pattern for case documented
- notation partially documented
- omitting the precedence level in a notation declaration is no longer allowed

fixed core notation

notation fixed to be NON associative by default

1. bug fixed in generalize_pattern: a lazy const_tac should have been
   relocated. The interesting case is

   generalize in match a in \vdash %

   where a occurs in the goal under at least one binder

2. pattern for cases partially implemented. It is now possible to perform
   a case on the hypotheses as long as the conclusion and hypothesis patterns
   are trivial (i.e. %)

- notation fixed according to the new stricter semantics
- generalize no longer required before case

- Procedural: we now check that an eliminator opens as many goals as the                      constructors of the eliminated type
              So nat_double_ind is not an eliminator for Nat :)
- Base-2    : now compiles correctly because we fixed the preamble :)

notation on steroids: 'term 40 x' is a valid variable name in notation and
places 'x' at term level 40 even if the notation is placed elsewhere

interpretation documented

initial support for notation that specifies the precedence of term variables, that allows to omit many useless parenthesis

removed unused variable

some work on Q

general reorganization and first (unconditional) proof of lebesgue over naturals

reordering of lexicon status partially avoided to make it sure
that interpretations are not moved around. I still argue that an alias can be
removed from the back of an interpretation, no idea how this would interfere with CSC recent patch

transformation from automath to intermediate language started

Dedekind sigma completeness for the natural numbers.

typo

some notation added with a bit PITA

final relevance check

copyright information added in the grundlagen text

when -debug do not catch

when -debug do not catch

replace assert false with AssertFailure

Initial version of the Helena Checker
- For now just parses an automath book (automath grammar by F. Wiedijg)
  the grundlagen is provided as (the only existing) example
- In the future will convert an automath book to a lambda-delta environment
  several lambda-delta extensions will be supported

New lemma
theorem eq_p_ord_q_O: ∀p,n,q. p_ord n p = pair ? ? q O → n=O ∧ q=O.

more notation

...

print the name not found in the env

Testing some performance tricks by caching the list of the first n primes and
showing that they are good either with nth_prime (sloooooooooowww) or with
sieve (slooooow and not proved correct yet). With sieve we are currently able
to verify the list of the first 103 primes in a sort of reasonable time.
The 103rd prime is only 593 :-(

better names in a lemma to increase readability

fixed some regressions

New, much faster implementation of factorize.

gran casino

meta not considered before in outtype

bla bla bla

relevance check for Match

initial qork for models

Added check of relevance lists for inductive types/constructors and
fixpoint definitions.

lebesgue proved

snapshot

Most of the time, URIs can now be replaced with identifiers in "interpretation".
Warning: identifiers are mapped to URIs according to the last declared
alias.

It is now possible to use identifiers in place of URI in "interpreation".
The identifier is mapped to an URI according to the last declared alias.

Reverting to the previous version some files which weren't intended to be
changed.

more proof irrelevance

initial work on lebesque

exhaustivity completed

exhaustivity, some work

generalize no more required before elim

generalize no more required before elim

generalize no more required before elim

generalize no more required before elim

generalize no more required by elim

Generalize no more required for elim.

generalize no more required before elim

generalize no more useful for elim

Bug fixed: wrong default pattern for generalize.

New: pattern for elim documented.

Hypotheses patterns for elim implemented. No more need to generalize in advance.

exhaustivity defined

proof simplified

Even more Q stuff moved around.

Even more Q stuff classified.

lemma 3.6 subverted

more stuff moved around

More Q stuff organized in a coherent way.

First snapshot at trying to clean up the Q library.

...

A new theorem

cleanup

Cleanup.

sieve.ma now depends only on primes.ma

Added frac.ma

Added Qplus_andrea.ma

Reduce reduction tactic got rid of a long time ago.

Eratosthene's sieve factorized out of nat/bertrand.ma. Nothing added not
removed.
In theory, sieve.ma ishould not depend on nth_prime.ma and factorization.ma.
In practice, a proof requires factorization that, in turn, depends on
nth_prime.ma. To be investigated.

....