commit by user ricciott

commit by user

urgent partial commit ... to be fixed later ...

urgent partial commit ... to be fixed later ...

update in basic_2

- some work on context equivalence of atomic arity assignment

Added in basics
- vectors.ma
- finset.ma

Added turing

minor ntegrations in list,ma and listb.ma

Minor changes

More changes to the website (matitaweb).

Various updates to the (obsolete) website.

modifiche

Versione italiana

New home

Top picture

prova

Created a new directory for Matita1.0

additions to basic_2

- more on subject reduction of atomic arity assignment
- some results on context-sensitive equivalence of terms

manual commit

Matitaweb:

Improved support for notations enriched with hyperlinks.
This revision introduces a "ref" keyword which can be used in the lefthand side
of notation statements. "ref" can only be used to decorate literals (i.e.
symbols, numbers, or keywords). The syntax is as follows:

  LITERAL ::= SIMPLE_LITERAL
           |  ref CSYMBOL SIMPLE_LITERAL

For example, the notation

  ref 'cons [ list0 x sep ; ref 'nil ]

used as the compact notation for lists specifies that the `[' symbol will be
enriched with the interpretation of 'cons nodes of the AST, and the `]' symbol
with the interpretation of 'nil nodes of the AST.

additions in basic_2

- pts: we restored the former hierarchy
- nat: we added a missing lemma
- lambda_delta: subject reduction continues ...

Matitaweb: Fixes a bug in the extensible parser which caused Matita to crash
when parsing a notation using keywords (rather than symbols). The semantic
action associated to the notation was expecting the parser to decorate the
keyword token with its location: this was not happening, causing a runtime
type exception.

Matitaweb: Fixes a bug which prevented Mozilla from displaying long goals
correctly.

commit by user andrea

commit by user utente2

commit by user

commit by user ricciott

commit by user andrea

Matitaweb:
1) partially solves a problem with TeX-like macro conversion when the script contains markup
2) ports a bugfix from Matita 1.0 (see log for revision 11211).

additions to basic_2

- basics: bug fix in Conf3, it was not generic enough
- lambda_delta: subject reduction of static typestarted ...

update in basic_2 and apps_2

- basics: some support for abstract triangular confluence (which
subject reduction is an instance of)
- predefined_virtuals: more Alt-L shortcuts
- lambda_delta: more properties on computation, some annotations,
improved Makefile

renaming completed

some renaming (ld_ prefix removed from file names)

some renaming: ld_ prefix removed

milestone update in basic_2!

- lambda_delta: strong normalization of simply typed terms closed!
- star.ma: transitive closure: support for reverse elimination

Manual commit (basics/core_notation.ma)

update in basic_2

property S2 of strongly normalizing terms proved!

- property S4 of strongly normalizing term proved!

manual correction to tutorial/chapter2.ma

- Properties S3 and S5 of context-sensitive strongly normalizing terms
proved!
- more properties of context-sensitive computation

Matitaweb:

1) Solves a bug in "Del hrefs"

2) Solves interaction glitches related to the disambiguation/error
reporting interface

3) Fixes the implementation of the Upload feature

4) Adds support for "low-users", who don't have permission to commit

5) Solves problems related to the multi-user mode

6) Limits direct file access to the html/ subdir of the Matita
installation (for security); all the files that must be accessed by a
web browser have been moved there

7) utf8macrotable.js uses numeric html entities instead of named
entities, to cope with incoherent behaviour of web browsers (named
entities being resolved to different unicode characters -- possible
bug in the web browser).

8) disables many debug prints

- context-sensitive computation: more properties
- context-sensitive reduction: bug fix in a lemma's name
- some annotations added

generated web pages update

- renaming completed!
- one more property of context-sensitive computation
- improved Makefile (from former commit)

We are decapitalizing the contributions' names ...

- update in Basic_2
- we added some information in thesunnary tables

- lambda_delta: morew propertie in context-sensitive computation
- formal_topology: compilation of categories.ma continues ...
- grafiteEngine.ml: coercions to sorts can now be defined with the short
syntax

Fixes bug where switching to a new tab the slider is not updated correctly.

commit by user andrea

commit by user andrea

commit by user andrea

commit by user utente2

commit by user ricciott

commit by user andrea

Axiom proved

Sectionin

commit by user utente2

commit by user andrea

more sections

small changes

Titols

Sections

commit by user andrea

commit by user utente2

section in chapter 2

commit by user andrea

Added sections in chapter 1.

Removed re.ma and re1.ma

commit by user andrea

commit by user andrea

commit by user andrea

commit by user andrea

commit by user utente2

commit by user ricciott

commit by user andrea

Forward compatibility with new releases of Camlp5.

Workaround for a BSD bug (submitted by Boender).

Bug fixed: horizontal scrolling now works correctly when the tab is changed.
The patch, however, is costly (everything is re-drawn twice).

MAJOR SPEED UP. The previous implementation of scrolling of the slidebar to
the end of the sequent was based on listening to signals. These signals:

1) were raised multiple times for each insertion (LOT of times!) making
   the scrolling extremely slow.
2) the callback was registered multiple times every time the user switched
   goal. This made the system slower and slower.

Minor speed up in the code.

commit by user andrea

Removed gif

chapter 9

Pictures

commit by user andrea

commit by user andrea

commit by user andrea

Small changes

Major speed-up improvement. Adding one callback per hyperlink was
extremely costly. It is now immediate.

chapter 9 and 10

commit by user andrea

- lambda_delta: "conversion" and "equivalence" components started
- formal_topology: porting to lib started. cprop_connectives compiles!

commit by user andrea

commit by user andrea