]> matita.cs.unibo.it Git - helm.git/log
helm.git
12 years agomilestone update in basic_2!
Ferruccio Guidi [Thu, 15 Mar 2012 18:27:33 +0000 (18:27 +0000)]
milestone update in basic_2!

12 years ago- lambda_delta: strong normalization of simply typed terms closed!
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

12 years agoManual commit (basics/core_notation.ma)
matitaweb [Thu, 15 Mar 2012 10:33:00 +0000 (10:33 +0000)]
Manual commit (basics/core_notation.ma)

12 years agoupdate in basic_2
Ferruccio Guidi [Wed, 14 Mar 2012 20:04:04 +0000 (20:04 +0000)]
update in basic_2

12 years agoproperty S2 of strongly normalizing terms proved!
Ferruccio Guidi [Wed, 14 Mar 2012 19:53:16 +0000 (19:53 +0000)]
property S2 of strongly normalizing terms proved!

12 years ago- property S4 of strongly normalizing term proved!
Ferruccio Guidi [Wed, 14 Mar 2012 15:39:49 +0000 (15:39 +0000)]
- property S4 of strongly normalizing term proved!

12 years agomanual correction to tutorial/chapter2.ma
matitaweb [Tue, 13 Mar 2012 15:12:07 +0000 (15:12 +0000)]
manual correction to tutorial/chapter2.ma

12 years ago- Properties S3 and S5 of context-sensitive strongly normalizing terms
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

12 years ago(no commit message)
matitaweb [Mon, 12 Mar 2012 14:56:10 +0000 (14:56 +0000)]

12 years agoMatitaweb:
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

12 years ago- context-sensitive computation: more properties
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

12 years agogenerated web pages update
Ferruccio Guidi [Sat, 10 Mar 2012 19:07:03 +0000 (19:07 +0000)]
generated web pages update

12 years ago- renaming completed!
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)

12 years agoWe are decapitalizing the contributions' names ...
Ferruccio Guidi [Sat, 10 Mar 2012 14:46:11 +0000 (14:46 +0000)]
We are decapitalizing the contributions' names ...

12 years ago- update in Basic_2
Ferruccio Guidi [Fri, 9 Mar 2012 17:38:40 +0000 (17:38 +0000)]
- update in Basic_2
- we added some information in thesunnary tables

12 years ago- lambda_delta: morew propertie in context-sensitive computation
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

12 years agoFixes bug where switching to a new tab the slider is not updated correctly.
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.

12 years agocommit by user andrea
matitaweb [Thu, 8 Mar 2012 10:02:01 +0000 (10:02 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Thu, 8 Mar 2012 08:24:25 +0000 (08:24 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Thu, 8 Mar 2012 07:55:11 +0000 (07:55 +0000)]
commit by user andrea

12 years agocommit by user utente2
matitaweb [Thu, 8 Mar 2012 07:43:40 +0000 (07:43 +0000)]
commit by user utente2

12 years agocommit by user ricciott
matitaweb [Thu, 8 Mar 2012 07:43:23 +0000 (07:43 +0000)]
commit by user ricciott

12 years agocommit by user andrea
matitaweb [Thu, 8 Mar 2012 07:43:21 +0000 (07:43 +0000)]
commit by user andrea

12 years agoAxiom proved
Andrea Asperti [Thu, 8 Mar 2012 07:38:38 +0000 (07:38 +0000)]
Axiom proved

12 years agoSectionin
matitaweb [Thu, 8 Mar 2012 07:21:22 +0000 (07:21 +0000)]
Sectionin

12 years agocommit by user utente2
matitaweb [Wed, 7 Mar 2012 11:50:58 +0000 (11:50 +0000)]
commit by user utente2

12 years agocommit by user andrea
matitaweb [Wed, 7 Mar 2012 11:50:55 +0000 (11:50 +0000)]
commit by user andrea

12 years agomore sections
matitaweb [Wed, 7 Mar 2012 11:47:26 +0000 (11:47 +0000)]
more sections

12 years agosmall changes
matitaweb [Wed, 7 Mar 2012 11:41:23 +0000 (11:41 +0000)]
small changes

12 years agoTitols
matitaweb [Wed, 7 Mar 2012 11:40:06 +0000 (11:40 +0000)]
Titols

12 years agoSections
matitaweb [Wed, 7 Mar 2012 11:37:19 +0000 (11:37 +0000)]
Sections

12 years agocommit by user andrea
matitaweb [Wed, 7 Mar 2012 10:37:08 +0000 (10:37 +0000)]
commit by user andrea

12 years agocommit by user utente2
matitaweb [Wed, 7 Mar 2012 10:37:05 +0000 (10:37 +0000)]
commit by user utente2

12 years agosection in chapter 2
matitaweb [Wed, 7 Mar 2012 10:26:46 +0000 (10:26 +0000)]
section in chapter 2

12 years agocommit by user andrea
matitaweb [Wed, 7 Mar 2012 10:13:47 +0000 (10:13 +0000)]
commit by user andrea

12 years agoAdded sections in chapter 1.
matitaweb [Wed, 7 Mar 2012 10:01:30 +0000 (10:01 +0000)]
Added sections in chapter 1.

12 years agoRemoved re.ma and re1.ma
matitaweb [Wed, 7 Mar 2012 09:04:02 +0000 (09:04 +0000)]
Removed re.ma and re1.ma

12 years agocommit by user andrea
matitaweb [Wed, 7 Mar 2012 08:46:44 +0000 (08:46 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Wed, 7 Mar 2012 08:45:22 +0000 (08:45 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Tue, 6 Mar 2012 18:24:11 +0000 (18:24 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Tue, 6 Mar 2012 18:09:27 +0000 (18:09 +0000)]
commit by user andrea

12 years agocommit by user utente2
matitaweb [Tue, 6 Mar 2012 18:01:38 +0000 (18:01 +0000)]
commit by user utente2

12 years agocommit by user ricciott
matitaweb [Tue, 6 Mar 2012 18:01:33 +0000 (18:01 +0000)]
commit by user ricciott

12 years agocommit by user andrea
matitaweb [Tue, 6 Mar 2012 18:01:27 +0000 (18:01 +0000)]
commit by user andrea

12 years agoForward compatibility with new releases of Camlp5.
Claudio Sacerdoti Coen [Tue, 6 Mar 2012 16:27:46 +0000 (16:27 +0000)]
Forward compatibility with new releases of Camlp5.

12 years agoWorkaround for a BSD bug (submitted by Boender).
Claudio Sacerdoti Coen [Tue, 6 Mar 2012 16:25:44 +0000 (16:25 +0000)]
Workaround for a BSD bug (submitted by Boender).

12 years agoBug fixed: horizontal scrolling now works correctly when the tab is changed.
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).

12 years agoMAJOR SPEED UP. The previous implementation of scrolling of the slidebar to
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.

12 years agoMinor speed up in the code.
Claudio Sacerdoti Coen [Tue, 6 Mar 2012 15:31:30 +0000 (15:31 +0000)]
Minor speed up in the code.

12 years agocommit by user andrea
matitaweb [Tue, 6 Mar 2012 13:56:12 +0000 (13:56 +0000)]
commit by user andrea

12 years agoRemoved gif
matitaweb [Tue, 6 Mar 2012 13:45:19 +0000 (13:45 +0000)]
Removed gif

12 years agochapter 9
matitaweb [Tue, 6 Mar 2012 13:44:53 +0000 (13:44 +0000)]
chapter 9

12 years agoPictures
matitaweb [Tue, 6 Mar 2012 12:45:54 +0000 (12:45 +0000)]
Pictures

12 years agocommit by user andrea
matitaweb [Tue, 6 Mar 2012 12:27:17 +0000 (12:27 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Tue, 6 Mar 2012 12:11:14 +0000 (12:11 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Tue, 6 Mar 2012 12:09:27 +0000 (12:09 +0000)]
commit by user andrea

12 years agoSmall changes
matitaweb [Tue, 6 Mar 2012 12:04:58 +0000 (12:04 +0000)]
Small changes

12 years agoMajor speed-up improvement. Adding one callback per hyperlink was
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.

12 years agochapter 9 and 10
matitaweb [Tue, 6 Mar 2012 11:44:26 +0000 (11:44 +0000)]
chapter 9 and 10

12 years agocommit by user andrea
matitaweb [Tue, 6 Mar 2012 11:37:20 +0000 (11:37 +0000)]
commit by user andrea

12 years ago- lambda_delta: "conversion" and "equivalence" components started
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!

12 years agocommit by user andrea
matitaweb [Fri, 2 Mar 2012 17:42:35 +0000 (17:42 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Fri, 2 Mar 2012 17:07:30 +0000 (17:07 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Fri, 2 Mar 2012 16:57:10 +0000 (16:57 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Fri, 2 Mar 2012 15:25:37 +0000 (15:25 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Fri, 2 Mar 2012 15:02:54 +0000 (15:02 +0000)]
commit by user andrea

12 years agocommit by user utente2
matitaweb [Fri, 2 Mar 2012 09:42:54 +0000 (09:42 +0000)]
commit by user utente2

12 years agocommit by user andrea
matitaweb [Fri, 2 Mar 2012 09:42:52 +0000 (09:42 +0000)]
commit by user andrea

12 years agoSplitted chapter 7
matitaweb [Fri, 2 Mar 2012 09:02:13 +0000 (09:02 +0000)]
Splitted chapter 7

12 years agocommit by user andrea
matitaweb [Fri, 2 Mar 2012 08:49:27 +0000 (08:49 +0000)]
commit by user andrea

12 years agomissing files in the former commit :(
Ferruccio Guidi [Thu, 1 Mar 2012 21:01:30 +0000 (21:01 +0000)]
missing files in the former commit :(

12 years agocommit by user andrea
matitaweb [Thu, 1 Mar 2012 17:52:50 +0000 (17:52 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Thu, 1 Mar 2012 16:38:03 +0000 (16:38 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Thu, 1 Mar 2012 13:00:50 +0000 (13:00 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Wed, 29 Feb 2012 12:26:57 +0000 (12:26 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Wed, 29 Feb 2012 11:54:56 +0000 (11:54 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Wed, 29 Feb 2012 11:31:22 +0000 (11:31 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Wed, 29 Feb 2012 10:45:22 +0000 (10:45 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Tue, 28 Feb 2012 13:59:14 +0000 (13:59 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Tue, 28 Feb 2012 13:55:24 +0000 (13:55 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Tue, 28 Feb 2012 13:17:46 +0000 (13:17 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Tue, 28 Feb 2012 13:11:17 +0000 (13:11 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Tue, 28 Feb 2012 09:29:28 +0000 (09:29 +0000)]
commit by user andrea

12 years agocommit by user utente2
matitaweb [Tue, 28 Feb 2012 08:23:15 +0000 (08:23 +0000)]
commit by user utente2

12 years agocommit by user andrea
matitaweb [Tue, 28 Feb 2012 08:23:11 +0000 (08:23 +0000)]
commit by user andrea

12 years agosome additions to Basic_2
Ferruccio Guidi [Mon, 27 Feb 2012 21:46:51 +0000 (21:46 +0000)]
some additions to Basic_2

12 years ago- property S6 of stronfly normalizing terms proved
Ferruccio Guidi [Mon, 27 Feb 2012 21:43:36 +0000 (21:43 +0000)]
- property S6 of stronfly normalizing terms proved
- more properties concerning context sensitive computation

12 years agosite update
Ferruccio Guidi [Fri, 24 Feb 2012 18:21:09 +0000 (18:21 +0000)]
site update

12 years ago- we added a web page (Apps_2) for the checked applications of Basic_2
Ferruccio Guidi [Fri, 24 Feb 2012 16:27:56 +0000 (16:27 +0000)]
- we added a web page (Apps_2) for the checked applications of Basic_2
- we added some files to Basic_2
- we improved the Makefiles

12 years ago- "functional" component moved to Apps_2
Ferruccio Guidi [Fri, 24 Feb 2012 12:53:09 +0000 (12:53 +0000)]
- "functional" component moved to Apps_2
- property S5 of the candidates of reducibility almost proved ...

12 years agocommit by user andrea
matitaweb [Thu, 23 Feb 2012 10:46:38 +0000 (10:46 +0000)]
commit by user andrea

12 years agorefiner porting from matita 1.
Wilmer Ricciotti [Thu, 23 Feb 2012 09:48:07 +0000 (09:48 +0000)]
refiner porting from matita 1.

12 years agoIntegrations
matitaweb [Wed, 22 Feb 2012 12:31:42 +0000 (12:31 +0000)]
Integrations

12 years agoComplete outline. Raw scripts.
matitaweb [Wed, 22 Feb 2012 09:28:17 +0000 (09:28 +0000)]
Complete outline. Raw scripts.

12 years ago- more properties on strongly normalizing terms ...
Ferruccio Guidi [Tue, 21 Feb 2012 18:30:32 +0000 (18:30 +0000)]
- more properties on strongly normalizing terms ...

12 years ago- site update
Ferruccio Guidi [Tue, 21 Feb 2012 10:37:41 +0000 (10:37 +0000)]
- site update

12 years agoadditions to Basic_2 ...
Ferruccio Guidi [Mon, 20 Feb 2012 19:11:10 +0000 (19:11 +0000)]
additions to Basic_2 ...

12 years agoinitial properies of the "same top term constructor" predicate
Ferruccio Guidi [Mon, 20 Feb 2012 18:59:54 +0000 (18:59 +0000)]
initial properies of the "same top term constructor" predicate

12 years agomore results on strongly normalizing terms
Ferruccio Guidi [Sat, 18 Feb 2012 19:16:56 +0000 (19:16 +0000)]
more results on strongly normalizing terms

12 years agoadditions to Basic_2
Ferruccio Guidi [Tue, 14 Feb 2012 20:16:38 +0000 (20:16 +0000)]
additions to Basic_2