]>
matita.cs.unibo.it Git - helm.git/log
Andrea Asperti [Tue, 11 May 2010 08:50:33 +0000 (08:50 +0000)]
minimization.ma
Enrico Tassi [Tue, 11 May 2010 07:21:34 +0000 (07:21 +0000)]
little workaround for multiple screens, gdk support not bound by lablgtk2
Enrico Tassi [Mon, 10 May 2010 09:48:33 +0000 (09:48 +0000)]
new intro:
Enrico Tassi [Fri, 7 May 2010 21:21:01 +0000 (21:21 +0000)]
trace generation with "// by _;"
Enrico Tassi [Fri, 7 May 2010 21:20:58 +0000 (21:20 +0000)]
notation
Andrea Asperti [Fri, 7 May 2010 10:04:00 +0000 (10:04 +0000)]
remarks and applyS
Claudio Sacerdoti Coen [Thu, 6 May 2010 22:35:02 +0000 (22:35 +0000)]
Bug fixed: nstatus => status (to undo the changes).
Claudio Sacerdoti Coen [Thu, 6 May 2010 15:52:38 +0000 (15:52 +0000)]
...
Wilmer Ricciotti [Thu, 6 May 2010 15:50:07 +0000 (15:50 +0000)]
Fixing naming scheme for composite coercions.
Claudio Sacerdoti Coen [Thu, 6 May 2010 15:45:35 +0000 (15:45 +0000)]
assert false could happen
Claudio Sacerdoti Coen [Thu, 6 May 2010 15:15:46 +0000 (15:15 +0000)]
Bug fixed:
Claudio Sacerdoti Coen [Wed, 5 May 2010 15:13:41 +0000 (15:13 +0000)]
coinduction is between us
Claudio Sacerdoti Coen [Wed, 5 May 2010 14:29:57 +0000 (14:29 +0000)]
First tests.
Wilmer Ricciotti [Tue, 4 May 2010 16:49:59 +0000 (16:49 +0000)]
* Fixed a couple of glitches in ndestruct
Claudio Sacerdoti Coen [Tue, 4 May 2010 16:40:26 +0000 (16:40 +0000)]
Regular expressions.
Ferruccio Guidi [Wed, 21 Apr 2010 09:00:04 +0000 (09:00 +0000)]
new dependences
From: fguidi <fguidi@
c2b2084f -9a08-0410-b176-
e24b037a169a >
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 >
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 >
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 >
Claudio Sacerdoti Coen [Wed, 14 Apr 2010 15:47:51 +0000 (15:47 +0000)]
...
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Claudio Sacerdoti Coen [Wed, 14 Apr 2010 14:06:35 +0000 (14:06 +0000)]
...
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Claudio Sacerdoti Coen [Wed, 14 Apr 2010 13:42:14 +0000 (13:42 +0000)]
Formal points.
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
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 >
Enrico Tassi [Tue, 13 Apr 2010 19:56:18 +0000 (19:56 +0000)]
fixed makefile
From: tassi <tassi@
c2b2084f -9a08-0410-b176-
e24b037a169a >
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 >
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 >
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 >
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 >
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 >
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 >
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 >
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 >
Enrico Tassi [Thu, 8 Apr 2010 17:49:30 +0000 (17:49 +0000)]
...
From: tassi <tassi@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Enrico Tassi [Thu, 8 Apr 2010 17:44:46 +0000 (17:44 +0000)]
support axioms
From: tassi <tassi@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Enrico Tassi [Thu, 8 Apr 2010 17:33:28 +0000 (17:33 +0000)]
...
From: tassi <tassi@
c2b2084f -9a08-0410-b176-
e24b037a169a >
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 >
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 >
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 >
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 >
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 >
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 >
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 >
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 >
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 >
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 >
Claudio Sacerdoti Coen [Wed, 31 Mar 2010 14:40:34 +0000 (14:40 +0000)]
...
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
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 >
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 >
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 >
Claudio Sacerdoti Coen [Wed, 31 Mar 2010 13:31:23 +0000 (13:31 +0000)]
ninversion
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Andrea Asperti [Wed, 31 Mar 2010 10:29:30 +0000 (10:29 +0000)]
removed boh
From: asperti <asperti@
c2b2084f -9a08-0410-b176-
e24b037a169a >
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 >
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 >
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 >
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 >
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 >
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 >
Matthias Puech [Thu, 25 Mar 2010 16:23:10 +0000 (16:23 +0000)]
Automation problem
From: puech <puech@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Andrea Asperti [Thu, 25 Mar 2010 14:22:31 +0000 (14:22 +0000)]
More work
From: asperti <asperti@
c2b2084f -9a08-0410-b176-
e24b037a169a >
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 >
Claudio Sacerdoti Coen [Thu, 25 Mar 2010 09:12:41 +0000 (09:12 +0000)]
...
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Andrea Asperti [Thu, 25 Mar 2010 08:41:21 +0000 (08:41 +0000)]
Conflict(?).
From: asperti <asperti@
c2b2084f -9a08-0410-b176-
e24b037a169a >
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 >
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 >
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 >
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 >
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 >
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 >
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 17:27:01 +0000 (17:27 +0000)]
...
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
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 >
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 >
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 14:20:39 +0000 (14:20 +0000)]
...
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
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 >
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 >
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 >
Andrea Asperti [Tue, 23 Mar 2010 17:50:12 +0000 (17:50 +0000)]
One more case.
From: asperti <asperti@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Andrea Asperti [Tue, 23 Mar 2010 16:31:55 +0000 (16:31 +0000)]
Readded eqf_2.
From: asperti <asperti@
c2b2084f -9a08-0410-b176-
e24b037a169a >
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 >
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 >
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 >
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 >
Andrea Asperti [Tue, 23 Mar 2010 15:45:06 +0000 (15:45 +0000)]
"flat" function (subst unfolding)
From: asperti <asperti@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Andrea Asperti [Tue, 23 Mar 2010 07:32:33 +0000 (07:32 +0000)]
Keeping only lift_aux e subst_aux (renamed to lift and subst).
From: asperti <asperti@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Andrea Asperti [Tue, 23 Mar 2010 07:31:12 +0000 (07:31 +0000)]
Moved compare in a different file.
From: asperti <asperti@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Matthias Puech [Thu, 18 Mar 2010 17:44:52 +0000 (17:44 +0000)]
Downgrading level of infix notations involving \sup.
Andrea Asperti [Thu, 18 Mar 2010 11:36:56 +0000 (11:36 +0000)]
Porting alla nuova def. di negazione
Andrea Asperti [Thu, 18 Mar 2010 11:35:44 +0000 (11:35 +0000)]
Nuova versione di not.
Andrea Asperti [Thu, 18 Mar 2010 11:33:10 +0000 (11:33 +0000)]
Printings removed.
Andrea Asperti [Thu, 18 Mar 2010 11:28:46 +0000 (11:28 +0000)]
Debugging disabled.
Andrea Asperti [Thu, 18 Mar 2010 11:28:22 +0000 (11:28 +0000)]
Debugging disabled.
Andrea Asperti [Thu, 18 Mar 2010 11:23:53 +0000 (11:23 +0000)]
New demodulation tactics (mostly for debugging purposes).
Andrea Asperti [Thu, 18 Mar 2010 11:22:11 +0000 (11:22 +0000)]
Exporting the demodulation function.
Andrea Asperti [Thu, 18 Mar 2010 11:19:53 +0000 (11:19 +0000)]
New option "demod" for auto.
Andrea Asperti [Thu, 18 Mar 2010 11:06:34 +0000 (11:06 +0000)]
Porting the new definition of equality.
Claudio Sacerdoti Coen [Thu, 18 Mar 2010 10:21:46 +0000 (10:21 +0000)]
Do not index examples (concrete syntax: nremark).
Claudio Sacerdoti Coen [Thu, 18 Mar 2010 10:21:14 +0000 (10:21 +0000)]
nremark => `Example (not to be indexed)
Andrea Asperti [Thu, 18 Mar 2010 07:18:36 +0000 (07:18 +0000)]
app of app inside smart application.
Ferruccio Guidi [Wed, 17 Mar 2010 15:10:12 +0000 (15:10 +0000)]
dr
Andrea Asperti [Wed, 17 Mar 2010 14:58:51 +0000 (14:58 +0000)]
qualche caso del lemma 5.2.11
Claudio Sacerdoti Coen [Wed, 17 Mar 2010 14:56:31 +0000 (14:56 +0000)]
OCaml's inferred type simplified.
projects / helm.git / log