]> matita.cs.unibo.it Git - helm.git/log
projects / helm.git / log
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
helm.git
14 years agoSome important proofs/definitions were (and are still) commented out and
commit | commitdiff | tree
Claudio Sacerdoti Coen [Sun, 4 Jul 2010 11:24:14 +0000 (11:24 +0000)]
Some important proofs/definitions were (and are still) commented out and
do not compile.

Added the notion of functor1 to state the main theorem.

14 years agoProof simplified.
commit | commitdiff | tree
Claudio Sacerdoti Coen [Thu, 1 Jul 2010 22:01:36 +0000 (22:01 +0000)]
Proof simplified.

14 years agoProof simplified (??).
commit | commitdiff | tree
Claudio Sacerdoti Coen [Thu, 1 Jul 2010 21:38:32 +0000 (21:38 +0000)]
Proof simplified (??).

14 years ago...
commit | commitdiff | tree
Enrico Tassi [Thu, 1 Jul 2010 16:52:00 +0000 (16:52 +0000)]
...

14 years ago...
commit | commitdiff | tree
Enrico Tassi [Wed, 30 Jun 2010 20:33:43 +0000 (20:33 +0000)]
...

14 years ago...
commit | commitdiff | tree
Enrico Tassi [Wed, 30 Jun 2010 14:10:39 +0000 (14:10 +0000)]
...

14 years ago...
commit | commitdiff | tree
Enrico Tassi [Wed, 30 Jun 2010 13:29:50 +0000 (13:29 +0000)]
...

14 years ago....
commit | commitdiff | tree
Enrico Tassi [Wed, 30 Jun 2010 09:44:22 +0000 (09:44 +0000)]
....

14 years ago...
commit | commitdiff | tree
Enrico Tassi [Tue, 29 Jun 2010 14:03:40 +0000 (14:03 +0000)]
...

14 years agonotation made half decent
commit | commitdiff | tree
Enrico Tassi [Tue, 29 Jun 2010 12:07:37 +0000 (12:07 +0000)]
notation made half decent

14 years agobetter notation for oalgebra
commit | commitdiff | tree
Enrico Tassi [Mon, 28 Jun 2010 20:15:28 +0000 (20:15 +0000)]
better notation for oalgebra

14 years ago....
commit | commitdiff | tree
Enrico Tassi [Fri, 18 Jun 2010 11:11:43 +0000 (11:11 +0000)]
....

14 years agooff by one fixed
commit | commitdiff | tree
Enrico Tassi [Thu, 17 Jun 2010 21:41:00 +0000 (21:41 +0000)]
off by one fixed

14 years agoFix for inversion principles of types with a single constructor.
commit | commitdiff | tree
Wilmer Ricciotti [Thu, 10 Jun 2010 18:23:59 +0000 (18:23 +0000)]
Fix for inversion principles of types with a single constructor.

14 years agoFixed a bug in the undebruijnate function which caused the refiner to produce
commit | commitdiff | tree
Wilmer Ricciotti [Tue, 8 Jun 2010 16:15:14 +0000 (16:15 +0000)]
Fixed a bug in the undebruijnate function which caused the refiner to produce
a wrong object when refining mutually recursive functions (the references to
recursive calls would contain the wrong index to the recursive argument).

14 years agosome stuff on re
commit | commitdiff | tree
Enrico Tassi [Mon, 7 Jun 2010 22:56:03 +0000 (22:56 +0000)]
some stuff on re

14 years agounify left args of inductive types with left argus of constructors. this allows
commit | commitdiff | tree
Enrico Tassi [Mon, 7 Jun 2010 22:55:47 +0000 (22:55 +0000)]
unify left args of inductive types with left argus of constructors. this allows
to put ? in every left arg of every constructor of an inductive type.

14 years agoLibrary support files for John Major equality and Russell.
commit | commitdiff | tree
Wilmer Ricciotti [Wed, 12 May 2010 18:41:47 +0000 (18:41 +0000)]
Library support files for John Major equality and Russell.

14 years agoExperimental support for Russell (coercions moving inside lambda & pattern
commit | commitdiff | tree
Wilmer Ricciotti [Wed, 12 May 2010 18:39:05 +0000 (18:39 +0000)]
Experimental support for Russell (coercions moving inside lambda & pattern
matching etc.) added to the refiner.

14 years agominimization.ma
commit | commitdiff | tree
Andrea Asperti [Tue, 11 May 2010 08:50:33 +0000 (08:50 +0000)]
minimization.ma

14 years agolittle workaround for multiple screens, gdk support not bound by lablgtk2
commit | commitdiff | tree
Enrico Tassi [Tue, 11 May 2010 07:21:34 +0000 (07:21 +0000)]
little workaround for multiple screens, gdk support not bound by lablgtk2

14 years agonew intro:
commit | commitdiff | tree
Enrico Tassi [Mon, 10 May 2010 09:48:33 +0000 (09:48 +0000)]
new intro:
- #; -- introduces into the context every possible assumption giving
        to it an unusable name
- #h1 .. h2; -- multi intros
- intros; -- macro che espande a #h1...hn.

14 years agotrace generation with "// by _;"
commit | commitdiff | tree
Enrico Tassi [Fri, 7 May 2010 21:21:01 +0000 (21:21 +0000)]
trace generation with "// by _;"

14 years agonotation
commit | commitdiff | tree
Enrico Tassi [Fri, 7 May 2010 21:20:58 +0000 (21:20 +0000)]
notation

14 years agoremarks and applyS
commit | commitdiff | tree
Andrea Asperti [Fri, 7 May 2010 10:04:00 +0000 (10:04 +0000)]
remarks and applyS

14 years agoBug fixed: nstatus => status (to undo the changes).
commit | commitdiff | tree
Claudio Sacerdoti Coen [Thu, 6 May 2010 22:35:02 +0000 (22:35 +0000)]
Bug fixed: nstatus => status (to undo the changes).

Worring warnings commented out.

14 years ago...
commit | commitdiff | tree
Claudio Sacerdoti Coen [Thu, 6 May 2010 15:52:38 +0000 (15:52 +0000)]
...

14 years agoFixing naming scheme for composite coercions.
commit | commitdiff | tree
Wilmer Ricciotti [Thu, 6 May 2010 15:50:07 +0000 (15:50 +0000)]
Fixing naming scheme for composite coercions.

14 years agoassert false could happen
commit | commitdiff | tree
Claudio Sacerdoti Coen [Thu, 6 May 2010 15:45:35 +0000 (15:45 +0000)]
assert false could happen

14 years agoBug fixed:
commit | commitdiff | tree
Claudio Sacerdoti Coen [Thu, 6 May 2010 15:15:46 +0000 (15:15 +0000)]
Bug fixed:

 During unification of E1 with E2, E1 and E2 where not always reduced.
 In particular, reduction was not performed in the cases:
   LetIn vs LetIn, Match vs Match
 and maybe also in some cases Appl Meta vs Appl Meta (who knows?)

14 years agocoinduction is between us
commit | commitdiff | tree
Claudio Sacerdoti Coen [Wed, 5 May 2010 15:13:41 +0000 (15:13 +0000)]
coinduction is between us

14 years agoFirst tests.
commit | commitdiff | tree
Claudio Sacerdoti Coen [Wed, 5 May 2010 14:29:57 +0000 (14:29 +0000)]
First tests.

14 years ago* Fixed a couple of glitches in ndestruct
commit | commitdiff | tree
Wilmer Ricciotti [Tue, 4 May 2010 16:49:59 +0000 (16:49 +0000)]
* Fixed a couple of glitches in ndestruct
  - blob equations were not always handled properly
  - tactic used to fail due to not optimal behaviour of the refiner
* Added (experimental) support for JM equality to ndestruct

14 years agoRegular expressions.
commit | commitdiff | tree
Claudio Sacerdoti Coen [Tue, 4 May 2010 16:40:26 +0000 (16:40 +0000)]
Regular expressions.

14 years agonew dependences
commit | commitdiff | tree
Ferruccio Guidi [Wed, 21 Apr 2010 09:00:04 +0000 (09:00 +0000)]
new dependences

From: fguidi <fguidi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoElimination of recursive inductive types leads to looping.
commit | commitdiff | tree
Andrea Asperti [Mon, 19 Apr 2010 09:47:02 +0000 (09:47 +0000)]
Elimination of recursive inductive types leads to looping.
ELimnation of singleton types gives problems with negation.

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoalpha_eq instead of pervasives.compare
commit | commitdiff | tree
Andrea Asperti [Mon, 19 Apr 2010 09:44:21 +0000 (09:44 +0000)]
alpha_eq instead of pervasives.compare

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agobool_ext on 'o' not on 'Prop' (they are convertible, but discrimination
commit | commitdiff | tree
Enrico Tassi [Thu, 15 Apr 2010 14:02:02 +0000 (14:02 +0000)]
bool_ext on 'o' not on 'Prop' (they are convertible, but discrimination
trees do not compare up to conversion)

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years ago...
commit | commitdiff | tree
Claudio Sacerdoti Coen [Wed, 14 Apr 2010 15:47:51 +0000 (15:47 +0000)]
...

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years ago...
commit | commitdiff | tree
Claudio Sacerdoti Coen [Wed, 14 Apr 2010 14:06:35 +0000 (14:06 +0000)]
...

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoFormal points.
commit | commitdiff | tree
Claudio Sacerdoti Coen [Wed, 14 Apr 2010 13:42:14 +0000 (13:42 +0000)]
Formal points.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoSome dualization clean-up.
commit | commitdiff | tree
Claudio Sacerdoti Coen [Wed, 14 Apr 2010 13:28:53 +0000 (13:28 +0000)]
Some dualization clean-up.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agofixed makefile
commit | commitdiff | tree
Enrico Tassi [Tue, 13 Apr 2010 19:56:18 +0000 (19:56 +0000)]
fixed makefile

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoauto destructs while introducing in the context
commit | commitdiff | tree
Enrico Tassi [Tue, 13 Apr 2010 19:55:18 +0000 (19:55 +0000)]
auto destructs while introducing in the context

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoprint nobjects (hack with Obj.magic)
commit | commitdiff | tree
Enrico Tassi [Tue, 13 Apr 2010 19:54:23 +0000 (19:54 +0000)]
print nobjects (hack with Obj.magic)

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agocatch the right exception, avoid uncaught Subst_not_found
commit | commitdiff | tree
Enrico Tassi [Tue, 13 Apr 2010 19:53:31 +0000 (19:53 +0000)]
catch the right exception, avoid uncaught Subst_not_found

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agosame heads different arity -> INCOMPARABLE
commit | commitdiff | tree
Enrico Tassi [Tue, 13 Apr 2010 19:52:58 +0000 (19:52 +0000)]
same heads different arity -> INCOMPARABLE

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agosome fixes to THF parser
commit | commitdiff | tree
Enrico Tassi [Tue, 13 Apr 2010 19:52:26 +0000 (19:52 +0000)]
some fixes to THF parser

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agofixed support file for TPTP
commit | commitdiff | tree
Enrico Tassi [Tue, 13 Apr 2010 19:51:39 +0000 (19:51 +0000)]
fixed support file for TPTP

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agothe edges must be quoted as well (not only the nodes)
commit | commitdiff | tree
Ferruccio Guidi [Sun, 11 Apr 2010 17:13:56 +0000 (17:13 +0000)]
the edges must be quoted as well (not only the nodes)

From: fguidi <fguidi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoapply_subst_context on statuses
commit | commitdiff | tree
Andrea Asperti [Fri, 9 Apr 2010 14:04:08 +0000 (14:04 +0000)]
apply_subst_context on statuses

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years ago...
commit | commitdiff | tree
Enrico Tassi [Thu, 8 Apr 2010 17:49:30 +0000 (17:49 +0000)]
...

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agosupport axioms
commit | commitdiff | tree
Enrico Tassi [Thu, 8 Apr 2010 17:44:46 +0000 (17:44 +0000)]
support axioms

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years ago...
commit | commitdiff | tree
Enrico Tassi [Thu, 8 Apr 2010 17:33:28 +0000 (17:33 +0000)]
...

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agothf problems list for tptp 4.0.1
commit | commitdiff | tree
Enrico Tassi [Thu, 8 Apr 2010 17:31:03 +0000 (17:31 +0000)]
thf problems list for tptp 4.0.1

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agofixed compiltion order of lexer/parser
commit | commitdiff | tree
Enrico Tassi [Thu, 8 Apr 2010 17:28:13 +0000 (17:28 +0000)]
fixed compiltion order of lexer/parser

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoNew code (unbranched) to compute all keys by all possible ways of reducing the term.
commit | commitdiff | tree
Claudio Sacerdoti Coen [Thu, 8 Apr 2010 16:38:53 +0000 (16:38 +0000)]
New code (unbranched) to compute all keys by all possible ways of reducing the term.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoNew sets of.
commit | commitdiff | tree
Claudio Sacerdoti Coen [Thu, 8 Apr 2010 16:37:26 +0000 (16:37 +0000)]
New sets of.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoTHF parser received some care
commit | commitdiff | tree
Enrico Tassi [Thu, 8 Apr 2010 14:43:43 +0000 (14:43 +0000)]
THF parser received some care

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoFixing indexing (commit parziale di Claudio?)
commit | commitdiff | tree
Andrea Asperti [Thu, 8 Apr 2010 13:02:05 +0000 (13:02 +0000)]
Fixing indexing (commit parziale di Claudio?)

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoTHF parser for TPTP
commit | commitdiff | tree
Enrico Tassi [Wed, 7 Apr 2010 13:34:29 +0000 (13:34 +0000)]
THF parser for TPTP

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoNot is now inductive.
commit | commitdiff | tree
Claudio Sacerdoti Coen [Wed, 31 Mar 2010 16:27:56 +0000 (16:27 +0000)]
Not is now inductive.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoUse the inversion!
commit | commitdiff | tree
Claudio Sacerdoti Coen [Wed, 31 Mar 2010 14:53:12 +0000 (14:53 +0000)]
Use the inversion!

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoBug fixed: the current equation is not always the last hyp.
commit | commitdiff | tree
Claudio Sacerdoti Coen [Wed, 31 Mar 2010 14:41:09 +0000 (14:41 +0000)]
Bug fixed: the current equation is not always the last hyp.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years ago...
commit | commitdiff | tree
Claudio Sacerdoti Coen [Wed, 31 Mar 2010 14:40:34 +0000 (14:40 +0000)]
...

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years ago- inversion principles are now generated also for co-inductive types
commit | commitdiff | tree
Claudio Sacerdoti Coen [Wed, 31 Mar 2010 13:49:43 +0000 (13:49 +0000)]
- inversion principles are now generated also for co-inductive types
- we use uniformly the cases_tac/elim_tac in the inversion principle

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoMore debugging info from print_tac.
commit | commitdiff | tree
Claudio Sacerdoti Coen [Wed, 31 Mar 2010 13:35:12 +0000 (13:35 +0000)]
More debugging info from print_tac.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoImplicit and UserInput were printed incorrectly.
commit | commitdiff | tree
Claudio Sacerdoti Coen [Wed, 31 Mar 2010 13:33:55 +0000 (13:33 +0000)]
Implicit and UserInput were printed incorrectly.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoninversion
commit | commitdiff | tree
Claudio Sacerdoti Coen [Wed, 31 Mar 2010 13:31:23 +0000 (13:31 +0000)]
ninversion

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoremoved boh
commit | commitdiff | tree
Andrea Asperti [Wed, 31 Mar 2010 10:29:30 +0000 (10:29 +0000)]
removed boh

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoAdded test file for inversion in ng matita.
commit | commitdiff | tree
Wilmer Ricciotti [Wed, 31 Mar 2010 09:39:37 +0000 (09:39 +0000)]
Added test file for inversion in ng matita.

From: ricciott <ricciott@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoTracing mechanism for auto. Interface changed to solve an ambiguity between
commit | commitdiff | tree
Andrea Asperti [Wed, 31 Mar 2010 09:07:11 +0000 (09:07 +0000)]
Tracing mechanism for auto. Interface changed to solve an ambiguity between
an ampty trace and a missing trace.

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoGood definition found.
commit | commitdiff | tree
Claudio Sacerdoti Coen [Fri, 26 Mar 2010 18:14:54 +0000 (18:14 +0000)]
Good definition found.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years ago(Co)Inductively Generated Formal Topologies (not only basic ones)
commit | commitdiff | tree
Claudio Sacerdoti Coen [Fri, 26 Mar 2010 17:27:53 +0000 (17:27 +0000)]
(Co)Inductively Generated Formal Topologies (not only basic ones)

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agopatched the definition of locate, advances in locate_add; still issues..
commit | commitdiff | tree
Matthias Puech [Thu, 25 Mar 2010 18:20:15 +0000 (18:20 +0000)]
patched the definition of locate, advances in locate_add; still issues..

From: puech <puech@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoZ.ma updated to reflect changes in the logical Not operator
commit | commitdiff | tree
Wilmer Ricciotti [Thu, 25 Mar 2010 18:00:49 +0000 (18:00 +0000)]
Z.ma updated to reflect changes in the logical Not operator

From: ricciott <ricciott@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoAutomation problem
commit | commitdiff | tree
Matthias Puech [Thu, 25 Mar 2010 16:23:10 +0000 (16:23 +0000)]
Automation problem

From: puech <puech@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoMore work
commit | commitdiff | tree
Andrea Asperti [Thu, 25 Mar 2010 14:22:31 +0000 (14:22 +0000)]
More work

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agocosi va (se vi pare).
commit | commitdiff | tree
Andrea Asperti [Thu, 25 Mar 2010 09:22:23 +0000 (09:22 +0000)]
cosi va (se vi pare).

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years ago...
commit | commitdiff | tree
Claudio Sacerdoti Coen [Thu, 25 Mar 2010 09:12:41 +0000 (09:12 +0000)]
...

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoConflict(?).
commit | commitdiff | tree
Andrea Asperti [Thu, 25 Mar 2010 08:41:21 +0000 (08:41 +0000)]
Conflict(?).

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoExtension of demod to arbtrary predicates (not just equalities).
commit | commitdiff | tree
Andrea Asperti [Thu, 25 Mar 2010 08:36:02 +0000 (08:36 +0000)]
Extension of demod to arbtrary predicates (not just equalities).

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoNice examples for automation (that fails).
commit | commitdiff | tree
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 17:56:32 +0000 (17:56 +0000)]
Nice examples for automation (that fails).

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoSimplified proof after pattern fix
commit | commitdiff | tree
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 17:48:45 +0000 (17:48 +0000)]
Simplified proof after pattern fix

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years ago"Not" is no longer a definition
commit | commitdiff | tree
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 17:36:05 +0000 (17:36 +0000)]
"Not" is no longer a definition

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoThe precedence of ^-1 has changed.
commit | commitdiff | tree
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 17:35:24 +0000 (17:35 +0000)]
The precedence of ^-1 has changed.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoEquality has one right parameter and thus it's elimination principle has two
commit | commitdiff | tree
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 17:33:09 +0000 (17:33 +0000)]
Equality has one right parameter and thus it's elimination principle has two
arguments to be protected by the scope, not 1. Why did I put one long ago in
place of 2? Maybe we were working on the old library where rewriting was non
dependent?

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years ago...
commit | commitdiff | tree
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 17:27:01 +0000 (17:27 +0000)]
...

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoAxioms were not indexed.
commit | commitdiff | tree
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 14:35:57 +0000 (14:35 +0000)]
Axioms were not indexed.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoAxioms were not indexed.
commit | commitdiff | tree
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 14:33:55 +0000 (14:33 +0000)]
Axioms were not indexed.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years ago...
commit | commitdiff | tree
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 14:20:39 +0000 (14:20 +0000)]
...

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoReal numbers as co-inductive streams of digits (overlapping refining intervals).
commit | commitdiff | tree
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 14:19:52 +0000 (14:19 +0000)]
Real numbers as co-inductive streams of digits (overlapping refining intervals).

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoComputation of the trace.
commit | commitdiff | tree
Andrea Asperti [Wed, 24 Mar 2010 13:04:27 +0000 (13:04 +0000)]
Computation of the trace.

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agotypo in a proof
commit | commitdiff | tree
Matthias Puech [Tue, 23 Mar 2010 18:24:49 +0000 (18:24 +0000)]
typo in a proof

From: puech <puech@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoOne more case.
commit | commitdiff | tree
Andrea Asperti [Tue, 23 Mar 2010 17:50:12 +0000 (17:50 +0000)]
One more case.

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoReadded eqf_2.
commit | commitdiff | tree
Andrea Asperti [Tue, 23 Mar 2010 16:31:55 +0000 (16:31 +0000)]
Readded eqf_2.

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agosymmetric_eq -> sym_eq
commit | commitdiff | tree
Andrea Asperti [Tue, 23 Mar 2010 15:59:10 +0000 (15:59 +0000)]
symmetric_eq -> sym_eq

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoRe-proved an axiom
commit | commitdiff | tree
Andrea Asperti [Tue, 23 Mar 2010 15:52:29 +0000 (15:52 +0000)]
Re-proved an axiom

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoCommented a few lemmas (copies).
commit | commitdiff | tree
Andrea Asperti [Tue, 23 Mar 2010 15:51:56 +0000 (15:51 +0000)]
Commented a few lemmas (copies).

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoFixed a few bugs
commit | commitdiff | tree
Andrea Asperti [Tue, 23 Mar 2010 15:48:42 +0000 (15:48 +0000)]
Fixed a few bugs

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

next
Unnamed repository; edit this file 'description' to name the repository.