]> matita.cs.unibo.it Git - helm.git/log
helm.git
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

12 years ago- more properties on strongly normalizing terms
Ferruccio Guidi [Tue, 14 Feb 2012 20:07:50 +0000 (20:07 +0000)]
- more properties on strongly normalizing terms
- bugfix in Basic_1 annotations

12 years agoadditions to Basic_2
Ferruccio Guidi [Sat, 11 Feb 2012 19:50:31 +0000 (19:50 +0000)]
additions to Basic_2

12 years ago- strong normalization of abbreviation proved
Ferruccio Guidi [Sat, 11 Feb 2012 19:48:08 +0000 (19:48 +0000)]
- strong normalization of abbreviation proved
- bug fix in the generation lemma for abbreviationof context=sensitive parallel reduction

12 years ago- design table for Basic_2
Ferruccio Guidi [Thu, 9 Feb 2012 19:51:29 +0000 (19:51 +0000)]
- design table for Basic_2
- summary table for Basic_2 and Ground_2
- some additions to the Basic_2 file table
- some new cell styles for xhtbl
- syntax cor comments added to xhtbl
- some improvements in the Makefiles

12 years ago- first properties of strongly normalizing terms
Ferruccio Guidi [Thu, 9 Feb 2012 19:30:41 +0000 (19:30 +0000)]
- first properties of strongly normalizing terms
- contex-sensitive normal forms
- context-sensitive parallel computation of terms

12 years ago- one file and three lemmas added to Basic 2
Ferruccio Guidi [Thu, 2 Feb 2012 18:43:22 +0000 (18:43 +0000)]
- one file and three lemmas added to Basic 2
- bugfix in Makefile

12 years ago- three lemmas on context sensitive parallel reduction closed
Ferruccio Guidi [Thu, 2 Feb 2012 18:29:52 +0000 (18:29 +0000)]
- three lemmas on context sensitive parallel reduction closed

12 years ago- notation fix for reducible and normal forms
Ferruccio Guidi [Wed, 1 Feb 2012 16:19:30 +0000 (16:19 +0000)]
- notation fix for reducible and normal forms
- some refactoring
- improved Makefile produces a table with numerical summary

12 years agothe Basic_2 page was not regenerated ...
Ferruccio Guidi [Wed, 1 Feb 2012 15:53:33 +0000 (15:53 +0000)]
the Basic_2 page was not regenerated ...

12 years agowe added summary and timeline to the Basic_2 page
Ferruccio Guidi [Wed, 1 Feb 2012 15:49:09 +0000 (15:49 +0000)]
we added summary and timeline to the Basic_2 page

12 years agoNotation for destructuring let-in for triples fixed.
Claudio Sacerdoti Coen [Tue, 31 Jan 2012 10:09:05 +0000 (10:09 +0000)]
Notation for destructuring let-in for triples fixed.

12 years ago- transitivity of lenv refinement for atomic arity asignment proved! ...
Ferruccio Guidi [Sun, 29 Jan 2012 16:05:55 +0000 (16:05 +0000)]
- transitivity of lenv refinement for atomic arity asignment proved! ...
- results on context-free normal forms refacored
- some annotation added

12 years agomore files added to Basic_2
Ferruccio Guidi [Sun, 29 Jan 2012 15:59:04 +0000 (15:59 +0000)]
more files added to Basic_2

12 years agosupport for abstract candidates of reducibility closed! ...
Ferruccio Guidi [Fri, 27 Jan 2012 21:01:01 +0000 (21:01 +0000)]
support for abstract candidates of reducibility closed! ...

12 years agomore files added to Basic_2
Ferruccio Guidi [Fri, 27 Jan 2012 20:54:52 +0000 (20:54 +0000)]
more files added to Basic_2

12 years agoFixes a bug in is_flexible (when checking a meta in subst, we did a recursive
Wilmer Ricciotti [Fri, 27 Jan 2012 14:31:20 +0000 (14:31 +0000)]
Fixes a bug in is_flexible (when checking a meta in subst, we did a recursive
call on its body without applying the local context, resulting in various
assertion failures).

12 years agoBetter error messages.
Claudio Sacerdoti Coen [Fri, 27 Jan 2012 14:25:42 +0000 (14:25 +0000)]
Better error messages.

12 years ago- one file added to Basic_2
Ferruccio Guidi [Thu, 26 Jan 2012 17:03:11 +0000 (17:03 +0000)]
- one file added to Basic_2

12 years ago- main lemmas about abstract reducibility candidates closed
Ferruccio Guidi [Thu, 26 Jan 2012 16:48:05 +0000 (16:48 +0000)]
- main lemmas about abstract reducibility candidates closed
- notation updated (and one bug solved)
- Makefile: stats display improved

12 years agoInversion principles generation falls back to cases tactic when elim is not
Wilmer Ricciotti [Mon, 23 Jan 2012 13:47:33 +0000 (13:47 +0000)]
Inversion principles generation falls back to cases tactic when elim is not
available.

12 years agobig fixin the structure of Basic_2
Ferruccio Guidi [Sat, 21 Jan 2012 21:28:26 +0000 (21:28 +0000)]
big fixin the structure of Basic_2

12 years agomore files to Basic_2
Ferruccio Guidi [Sat, 21 Jan 2012 21:16:02 +0000 (21:16 +0000)]
more files to Basic_2

12 years ago- main proof for strong normalization closed! ...
Ferruccio Guidi [Sat, 21 Jan 2012 21:05:57 +0000 (21:05 +0000)]
- main proof for strong normalization closed! ...
- bug fix in lenv refinement for abstract candidates of reducibility (lsubc)
- lenv refinement for atomic arity assignment defined (lsuba) and relation
with lsubc proved

12 years agoclosure property S4 added to abstract candidates of reducibility ...
Ferruccio Guidi [Thu, 19 Jan 2012 16:10:12 +0000 (16:10 +0000)]
closure property S4 added to abstract candidates of reducibility ...