]>
matita.cs.unibo.it Git - helm.git/log
Ferruccio Guidi [Wed, 4 Apr 2012 18:47:28 +0000 (18:47 +0000)]
- some work on context equivalence of atomic arity assignment
Andrea Asperti [Wed, 4 Apr 2012 07:28:38 +0000 (07:28 +0000)]
Added in basics
- vectors.ma
- finset.ma
Added turing
minor ntegrations in list,ma and listb.ma
Andrea Asperti [Tue, 3 Apr 2012 15:36:09 +0000 (15:36 +0000)]
Minor changes
Wilmer Ricciotti [Tue, 3 Apr 2012 13:33:04 +0000 (13:33 +0000)]
More changes to the website (matitaweb).
Wilmer Ricciotti [Tue, 3 Apr 2012 11:31:03 +0000 (11:31 +0000)]
Various updates to the (obsolete) website.
Andrea Asperti [Tue, 3 Apr 2012 10:37:54 +0000 (10:37 +0000)]
modifiche
Andrea Asperti [Tue, 3 Apr 2012 09:17:00 +0000 (09:17 +0000)]
Versione italiana
Andrea Asperti [Tue, 3 Apr 2012 08:55:02 +0000 (08:55 +0000)]
New home
Andrea Asperti [Tue, 3 Apr 2012 08:41:08 +0000 (08:41 +0000)]
Top picture
Andrea Asperti [Tue, 3 Apr 2012 08:35:11 +0000 (08:35 +0000)]
prova
Andrea Asperti [Tue, 3 Apr 2012 07:46:45 +0000 (07:46 +0000)]
Created a new directory for Matita1.0
Ferruccio Guidi [Fri, 30 Mar 2012 18:20:31 +0000 (18:20 +0000)]
additions to basic_2
Ferruccio Guidi [Fri, 30 Mar 2012 18:15:10 +0000 (18:15 +0000)]
- more on subject reduction of atomic arity assignment
- some results on context-sensitive equivalence of terms
matitaweb [Wed, 28 Mar 2012 08:22:32 +0000 (08:22 +0000)]
manual commit
Wilmer Ricciotti [Tue, 27 Mar 2012 12:23:00 +0000 (12:23 +0000)]
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.
Ferruccio Guidi [Fri, 23 Mar 2012 14:46:23 +0000 (14:46 +0000)]
additions in basic_2
Ferruccio Guidi [Fri, 23 Mar 2012 14:40:59 +0000 (14:40 +0000)]
- pts: we restored the former hierarchy
- nat: we added a missing lemma
- lambda_delta: subject reduction continues ...
Wilmer Ricciotti [Fri, 23 Mar 2012 10:24:22 +0000 (10:24 +0000)]
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.
Wilmer Ricciotti [Fri, 23 Mar 2012 10:11:15 +0000 (10:11 +0000)]
Matitaweb: Fixes a bug which prevented Mozilla from displaying long goals
correctly.
matitaweb [Fri, 23 Mar 2012 09:23:59 +0000 (09:23 +0000)]
commit by user andrea
matitaweb [Fri, 23 Mar 2012 08:52:03 +0000 (08:52 +0000)]
commit by user utente2
matitaweb [Fri, 23 Mar 2012 08:51:40 +0000 (08:51 +0000)]
commit by user
matitaweb [Fri, 23 Mar 2012 08:51:16 +0000 (08:51 +0000)]
commit by user ricciott
matitaweb [Fri, 23 Mar 2012 08:51:09 +0000 (08:51 +0000)]
commit by user andrea
matitaweb [Tue, 20 Mar 2012 16:27:14 +0000 (16:27 +0000)]
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).
Ferruccio Guidi [Mon, 19 Mar 2012 15:32:58 +0000 (15:32 +0000)]
additions to basic_2
Ferruccio Guidi [Mon, 19 Mar 2012 15:11:24 +0000 (15:11 +0000)]
- basics: bug fix in Conf3, it was not generic enough
- lambda_delta: subject reduction of static typestarted ...
Ferruccio Guidi [Sat, 17 Mar 2012 17:11:18 +0000 (17:11 +0000)]
update in basic_2 and apps_2
Ferruccio Guidi [Sat, 17 Mar 2012 16:51:06 +0000 (16:51 +0000)]
- 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
Ferruccio Guidi [Thu, 15 Mar 2012 19:03:49 +0000 (19:03 +0000)]
renaming completed
Ferruccio Guidi [Thu, 15 Mar 2012 18:57:05 +0000 (18:57 +0000)]
some renaming (ld_ prefix removed from file names)
Ferruccio Guidi [Thu, 15 Mar 2012 18:49:25 +0000 (18:49 +0000)]
some renaming: ld_ prefix removed
Ferruccio Guidi [Thu, 15 Mar 2012 18:27:33 +0000 (18:27 +0000)]
milestone update in basic_2!
Ferruccio Guidi [Thu, 15 Mar 2012 18:00:48 +0000 (18:00 +0000)]
- lambda_delta: strong normalization of simply typed terms closed!
- star.ma: transitive closure: support for reverse elimination
matitaweb [Thu, 15 Mar 2012 10:33:00 +0000 (10:33 +0000)]
Manual commit (basics/core_notation.ma)
Ferruccio Guidi [Wed, 14 Mar 2012 20:04:04 +0000 (20:04 +0000)]
update in basic_2
Ferruccio Guidi [Wed, 14 Mar 2012 19:53:16 +0000 (19:53 +0000)]
property S2 of strongly normalizing terms proved!
Ferruccio Guidi [Wed, 14 Mar 2012 15:39:49 +0000 (15:39 +0000)]
- property S4 of strongly normalizing term proved!
matitaweb [Tue, 13 Mar 2012 15:12:07 +0000 (15:12 +0000)]
manual correction to tutorial/chapter2.ma
Ferruccio Guidi [Mon, 12 Mar 2012 17:05:13 +0000 (17:05 +0000)]
- Properties S3 and S5 of context-sensitive strongly normalizing terms
proved!
- more properties of context-sensitive computation
matitaweb [Mon, 12 Mar 2012 14:56:10 +0000 (14:56 +0000)]
matitaweb [Mon, 12 Mar 2012 08:47:22 +0000 (08:47 +0000)]
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
Ferruccio Guidi [Sun, 11 Mar 2012 19:30:07 +0000 (19:30 +0000)]
- context-sensitive computation: more properties
- context-sensitive reduction: bug fix in a lemma's name
- some annotations added
Ferruccio Guidi [Sat, 10 Mar 2012 19:07:03 +0000 (19:07 +0000)]
generated web pages update
Ferruccio Guidi [Sat, 10 Mar 2012 19:03:31 +0000 (19:03 +0000)]
- renaming completed!
- one more property of context-sensitive computation
- improved Makefile (from former commit)
Ferruccio Guidi [Sat, 10 Mar 2012 14:46:11 +0000 (14:46 +0000)]
We are decapitalizing the contributions' names ...
Ferruccio Guidi [Fri, 9 Mar 2012 17:38:40 +0000 (17:38 +0000)]
- update in Basic_2
- we added some information in thesunnary tables
Ferruccio Guidi [Fri, 9 Mar 2012 17:31:33 +0000 (17:31 +0000)]
- 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
Claudio Sacerdoti Coen [Fri, 9 Mar 2012 16:34:21 +0000 (16:34 +0000)]
Fixes bug where switching to a new tab the slider is not updated correctly.
matitaweb [Thu, 8 Mar 2012 10:02:01 +0000 (10:02 +0000)]
commit by user andrea
matitaweb [Thu, 8 Mar 2012 08:24:25 +0000 (08:24 +0000)]
commit by user andrea
matitaweb [Thu, 8 Mar 2012 07:55:11 +0000 (07:55 +0000)]
commit by user andrea
matitaweb [Thu, 8 Mar 2012 07:43:40 +0000 (07:43 +0000)]
commit by user utente2
matitaweb [Thu, 8 Mar 2012 07:43:23 +0000 (07:43 +0000)]
commit by user ricciott
matitaweb [Thu, 8 Mar 2012 07:43:21 +0000 (07:43 +0000)]
commit by user andrea
Andrea Asperti [Thu, 8 Mar 2012 07:38:38 +0000 (07:38 +0000)]
Axiom proved
matitaweb [Thu, 8 Mar 2012 07:21:22 +0000 (07:21 +0000)]
Sectionin
matitaweb [Wed, 7 Mar 2012 11:50:58 +0000 (11:50 +0000)]
commit by user utente2
matitaweb [Wed, 7 Mar 2012 11:50:55 +0000 (11:50 +0000)]
commit by user andrea
matitaweb [Wed, 7 Mar 2012 11:47:26 +0000 (11:47 +0000)]
more sections
matitaweb [Wed, 7 Mar 2012 11:41:23 +0000 (11:41 +0000)]
small changes
matitaweb [Wed, 7 Mar 2012 11:40:06 +0000 (11:40 +0000)]
Titols
matitaweb [Wed, 7 Mar 2012 11:37:19 +0000 (11:37 +0000)]
Sections
matitaweb [Wed, 7 Mar 2012 10:37:08 +0000 (10:37 +0000)]
commit by user andrea
matitaweb [Wed, 7 Mar 2012 10:37:05 +0000 (10:37 +0000)]
commit by user utente2
matitaweb [Wed, 7 Mar 2012 10:26:46 +0000 (10:26 +0000)]
section in chapter 2
matitaweb [Wed, 7 Mar 2012 10:13:47 +0000 (10:13 +0000)]
commit by user andrea
matitaweb [Wed, 7 Mar 2012 10:01:30 +0000 (10:01 +0000)]
Added sections in chapter 1.
matitaweb [Wed, 7 Mar 2012 09:04:02 +0000 (09:04 +0000)]
Removed re.ma and re1.ma
matitaweb [Wed, 7 Mar 2012 08:46:44 +0000 (08:46 +0000)]
commit by user andrea
matitaweb [Wed, 7 Mar 2012 08:45:22 +0000 (08:45 +0000)]
commit by user andrea
matitaweb [Tue, 6 Mar 2012 18:24:11 +0000 (18:24 +0000)]
commit by user andrea
matitaweb [Tue, 6 Mar 2012 18:09:27 +0000 (18:09 +0000)]
commit by user andrea
matitaweb [Tue, 6 Mar 2012 18:01:38 +0000 (18:01 +0000)]
commit by user utente2
matitaweb [Tue, 6 Mar 2012 18:01:33 +0000 (18:01 +0000)]
commit by user ricciott
matitaweb [Tue, 6 Mar 2012 18:01:27 +0000 (18:01 +0000)]
commit by user andrea
Claudio Sacerdoti Coen [Tue, 6 Mar 2012 16:27:46 +0000 (16:27 +0000)]
Forward compatibility with new releases of Camlp5.
Claudio Sacerdoti Coen [Tue, 6 Mar 2012 16:25:44 +0000 (16:25 +0000)]
Workaround for a BSD bug (submitted by Boender).
Claudio Sacerdoti Coen [Tue, 6 Mar 2012 16:06:56 +0000 (16:06 +0000)]
Bug fixed: horizontal scrolling now works correctly when the tab is changed.
The patch, however, is costly (everything is re-drawn twice).
Claudio Sacerdoti Coen [Tue, 6 Mar 2012 15:35:29 +0000 (15:35 +0000)]
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.
Claudio Sacerdoti Coen [Tue, 6 Mar 2012 15:31:30 +0000 (15:31 +0000)]
Minor speed up in the code.
matitaweb [Tue, 6 Mar 2012 13:56:12 +0000 (13:56 +0000)]
commit by user andrea
matitaweb [Tue, 6 Mar 2012 13:45:19 +0000 (13:45 +0000)]
Removed gif
matitaweb [Tue, 6 Mar 2012 13:44:53 +0000 (13:44 +0000)]
chapter 9
matitaweb [Tue, 6 Mar 2012 12:45:54 +0000 (12:45 +0000)]
Pictures
matitaweb [Tue, 6 Mar 2012 12:27:17 +0000 (12:27 +0000)]
commit by user andrea
matitaweb [Tue, 6 Mar 2012 12:11:14 +0000 (12:11 +0000)]
commit by user andrea
matitaweb [Tue, 6 Mar 2012 12:09:27 +0000 (12:09 +0000)]
commit by user andrea
matitaweb [Tue, 6 Mar 2012 12:04:58 +0000 (12:04 +0000)]
Small changes
Claudio Sacerdoti Coen [Tue, 6 Mar 2012 11:45:57 +0000 (11:45 +0000)]
Major speed-up improvement. Adding one callback per hyperlink was
extremely costly. It is now immediate.
matitaweb [Tue, 6 Mar 2012 11:44:26 +0000 (11:44 +0000)]
chapter 9 and 10
matitaweb [Tue, 6 Mar 2012 11:37:20 +0000 (11:37 +0000)]
commit by user andrea
Ferruccio Guidi [Sun, 4 Mar 2012 19:23:00 +0000 (19:23 +0000)]
- lambda_delta: "conversion" and "equivalence" components started
- formal_topology: porting to lib started. cprop_connectives compiles!
matitaweb [Fri, 2 Mar 2012 17:42:35 +0000 (17:42 +0000)]
commit by user andrea
matitaweb [Fri, 2 Mar 2012 17:07:30 +0000 (17:07 +0000)]
commit by user andrea
matitaweb [Fri, 2 Mar 2012 16:57:10 +0000 (16:57 +0000)]
commit by user andrea
matitaweb [Fri, 2 Mar 2012 15:25:37 +0000 (15:25 +0000)]
commit by user andrea
matitaweb [Fri, 2 Mar 2012 15:02:54 +0000 (15:02 +0000)]
commit by user andrea
matitaweb [Fri, 2 Mar 2012 09:42:54 +0000 (09:42 +0000)]
commit by user utente2
matitaweb [Fri, 2 Mar 2012 09:42:52 +0000 (09:42 +0000)]
commit by user andrea