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

12 years agothe support for candidates of reducibility continues ...
Ferruccio Guidi [Mon, 16 Jan 2012 12:09:42 +0000 (12:09 +0000)]
the support for candidates of reducibility continues ...

12 years agosome additionsand refactoring in Basic_2
Ferruccio Guidi [Mon, 16 Jan 2012 12:06:47 +0000 (12:06 +0000)]
some additionsand refactoring in Basic_2

12 years agomore file names added to Basic_2
Ferruccio Guidi [Fri, 13 Jan 2012 15:44:30 +0000 (15:44 +0000)]
more file names added to Basic_2

12 years ago- the development of abstract reducibility candidates continues ...
Ferruccio Guidi [Fri, 13 Jan 2012 15:27:13 +0000 (15:27 +0000)]
- the development of abstract reducibility candidates continues ...
- some annotations added

12 years agoImproves the presentation of hypotheses in the goal pane.
Wilmer Ricciotti [Thu, 12 Jan 2012 12:03:29 +0000 (12:03 +0000)]
Improves the presentation of hypotheses in the goal pane.

12 years agoFixes r11788 (partial, thus broken commit).
Wilmer Ricciotti [Wed, 11 Jan 2012 10:45:07 +0000 (10:45 +0000)]
Fixes r11788 (partial, thus broken commit).

12 years agounpatched version for the new CamplP5
Ferruccio Guidi [Tue, 10 Jan 2012 20:42:17 +0000 (20:42 +0000)]
unpatched version for the new CamplP5

12 years agopatched version for old CamlP5
Ferruccio Guidi [Tue, 10 Jan 2012 20:31:44 +0000 (20:31 +0000)]
patched version for old CamlP5

12 years agoBugfix: NCicUnification.could_reduce now performs whd in the applied fixpoint
Wilmer Ricciotti [Tue, 10 Jan 2012 14:28:55 +0000 (14:28 +0000)]
Bugfix: NCicUnification.could_reduce now performs whd in the applied fixpoint
case, to prevent the recursive call from raising assert failure.

12 years agoA complete snapshot for re
Andrea Asperti [Tue, 10 Jan 2012 08:31:46 +0000 (08:31 +0000)]
A complete snapshot for re

12 years agomore characters shortcuts
Ferruccio Guidi [Sun, 8 Jan 2012 15:52:10 +0000 (15:52 +0000)]
more characters shortcuts

12 years agoBasic_2: restyling and more notation
Ferruccio Guidi [Sun, 8 Jan 2012 15:50:57 +0000 (15:50 +0000)]
Basic_2: restyling and more notation

12 years ago- notation restyling ...
Ferruccio Guidi [Sun, 8 Jan 2012 15:01:27 +0000 (15:01 +0000)]
- notation restyling ...

12 years agoBasic_2: - we addedsome files
Ferruccio Guidi [Sat, 7 Jan 2012 22:11:51 +0000 (22:11 +0000)]
Basic_2: - we addedsome files
         - we added some notation
 - we updated the table style

12 years agolambda_delta: global environments handling: redefined and first results
Ferruccio Guidi [Sat, 7 Jan 2012 19:29:46 +0000 (19:29 +0000)]
lambda_delta: global environments handling: redefined and first results
              rtm: first definitions
lib/arithmetics/nat: a missing lemma added
predefined_virtuals: we added circled numbers, circled letters and
other characters
depend, depend.opt: regenerated

12 years agothe support for reducibility candidates evolves ,,,,
Ferruccio Guidi [Wed, 4 Jan 2012 16:32:04 +0000 (16:32 +0000)]
the support for reducibility candidates evolves ,,,,

12 years agoComplete version
Andrea Asperti [Tue, 3 Jan 2012 16:16:45 +0000 (16:16 +0000)]
Complete version

12 years agomodified definition of memb
Andrea Asperti [Tue, 3 Jan 2012 16:00:01 +0000 (16:00 +0000)]
modified definition of memb

12 years agoreverse
Andrea Asperti [Tue, 3 Jan 2012 15:58:23 +0000 (15:58 +0000)]
reverse

12 years agomore properties of union
Andrea Asperti [Tue, 3 Jan 2012 15:57:18 +0000 (15:57 +0000)]
more properties of union

12 years agonoteq_to_eqnot
Andrea Asperti [Tue, 3 Jan 2012 15:55:51 +0000 (15:55 +0000)]
noteq_to_eqnot