]> matita.cs.unibo.it Git - helm.git/log
helm.git
23 years agoThis commit was manufactured by cvs2svn to create tag uwobo_pre_ocaml
no author [Mon, 12 Nov 2001 09:48:12 +0000 (09:48 +0000)]
This commit was manufactured by cvs2svn to create tag
'uwobo_pre_ocaml'.

23 years agoVersion 1.2.1beta => 1.2.1
Claudio Sacerdoti Coen [Mon, 12 Nov 2001 09:48:12 +0000 (09:48 +0000)]
Version 1.2.1beta => 1.2.1

23 years ago- Stylesheet exceptions now printed in red.
Claudio Sacerdoti Coen [Mon, 12 Nov 2001 09:37:39 +0000 (09:37 +0000)]
- Stylesheet exceptions now printed in red.
- Load of an already loaded stylesheet now ignored (was interpreted as
  reloadin before).
- Version renumbered as 1.2.1beta.

23 years agoCode cleanup: more code sharing achieved.
Claudio Sacerdoti Coen [Mon, 12 Nov 2001 09:22:27 +0000 (09:22 +0000)]
Code cleanup: more code sharing achieved.

23 years agoBug fixed: xsl:import not first child of xsl:stylesheet.
Claudio Sacerdoti Coen [Mon, 12 Nov 2001 09:04:20 +0000 (09:04 +0000)]
Bug fixed: xsl:import not first child of xsl:stylesheet.

23 years agoBug fixed: unbound variable.
Claudio Sacerdoti Coen [Mon, 12 Nov 2001 09:03:46 +0000 (09:03 +0000)]
Bug fixed: unbound variable.

23 years agoAdded "/getempty" method.
Stefano Zacchiroli [Sun, 11 Nov 2001 14:09:35 +0000 (14:09 +0000)]
Added "/getempty" method.
----
Syntax: "/getempty".
Answer: a minimal valid XML document.
Currently, the returned document is as follows:

  <?xml version="1.0"?>
  <!DOCTYPE empty [
    <!ELEMENT empty EMPTY>
  ]>
  <empty />

----

23 years agobinary ignored
Luca Padovani [Sat, 10 Nov 2001 19:17:47 +0000 (19:17 +0000)]
binary ignored

23 years ago.deps ignored
Luca Padovani [Sat, 10 Nov 2001 19:17:19 +0000 (19:17 +0000)]
.deps ignored

23 years ago- new handling of links
Luca Padovani [Sat, 10 Nov 2001 19:16:54 +0000 (19:16 +0000)]
- new handling of links
- no more conflict between links and actions (links have precedence)
- cursors now handled by helmpot
- fixed problem with pot cursor

23 years ago- added method to check for an attribute in a given namespace
Luca Padovani [Sat, 10 Nov 2001 19:15:55 +0000 (19:15 +0000)]
- added method to check for an attribute in a given namespace

23 years agoCode improvement: more code shared.
Claudio Sacerdoti Coen [Fri, 9 Nov 2001 18:45:44 +0000 (18:45 +0000)]
Code improvement: more code shared.

23 years agoSmall bug fixed.
Claudio Sacerdoti Coen [Fri, 9 Nov 2001 12:37:44 +0000 (12:37 +0000)]
Small bug fixed.

23 years agoThe body of the variables was not printed.
Claudio Sacerdoti Coen [Fri, 9 Nov 2001 10:00:19 +0000 (10:00 +0000)]
The body of the variables was not printed.

23 years agoindent="yes" in xsl:output removed to impreve performance.
Claudio Sacerdoti Coen [Fri, 9 Nov 2001 09:49:44 +0000 (09:49 +0000)]
indent="yes" in xsl:output removed to impreve performance.

23 years agoindent="yes" in xsl:output removed for performance increase.
Claudio Sacerdoti Coen [Fri, 9 Nov 2001 09:31:33 +0000 (09:31 +0000)]
indent="yes" in xsl:output removed for performance increase.

23 years agoThe same patch I have applied in the previous commit to m:ci has been
Claudio Sacerdoti Coen [Thu, 8 Nov 2001 18:47:12 +0000 (18:47 +0000)]
The same patch I have applied in the previous commit to m:ci has been
applied to m:mn.

23 years agoThe patch of Irene to allow MathML presentation inside <m:ci>
Claudio Sacerdoti Coen [Thu, 8 Nov 2001 18:07:59 +0000 (18:07 +0000)]
The patch of Irene to allow MathML presentation inside <m:ci>
was not correct. As a consequence (but there were worst ones)
hyperlinks were not created to sub-scripted identifiers.
I have changed the patch. Though, I am not sure it is the correct one.
In particular, what happens if I put content markup inside the m:ci?
(It was recursively processed in the original stylesheet)

23 years agoWorkaround replacement: instead of a litteral URL (path on disk), a litteral
Claudio Sacerdoti Coen [Thu, 8 Nov 2001 16:30:54 +0000 (16:30 +0000)]
Workaround replacement: instead of a litteral URL (path on disk), a litteral
request to the Getter on phd to resolve the URL.
The real problem (avoiding at all the thing) is still to be addressed.

23 years agoBug (that I introduced in my last commit to solve the problem of the
Claudio Sacerdoti Coen [Thu, 8 Nov 2001 16:27:42 +0000 (16:27 +0000)]
Bug (that I introduced in my last commit to solve the problem of the
free variable $id appearing everywhere in the notation for LAMBDA) fixed.
Now hyperlinks should be generated correctly.

23 years ago...
Claudio Sacerdoti Coen [Wed, 7 Nov 2001 18:44:41 +0000 (18:44 +0000)]
...

23 years agoGPL licence added
Claudio Sacerdoti Coen [Wed, 7 Nov 2001 18:43:38 +0000 (18:43 +0000)]
GPL licence added

23 years ago.cvsignore added
Claudio Sacerdoti Coen [Wed, 7 Nov 2001 18:43:11 +0000 (18:43 +0000)]
.cvsignore added

23 years agoXalan-J_2.2.D3
Claudio Sacerdoti Coen [Wed, 7 Nov 2001 18:32:07 +0000 (18:32 +0000)]
Xalan-J_2.2.D3

23 years agoxerces required by Xalan-J_2.2.D3
Claudio Sacerdoti Coen [Wed, 7 Nov 2001 18:30:53 +0000 (18:30 +0000)]
xerces required by Xalan-J_2.2.D3

23 years agoGPL licence added.
Claudio Sacerdoti Coen [Wed, 7 Nov 2001 18:23:06 +0000 (18:23 +0000)]
GPL licence added.

23 years agoVersion 1.2 ==> 1.2.0
Claudio Sacerdoti Coen [Tue, 6 Nov 2001 18:55:50 +0000 (18:55 +0000)]
Version 1.2 ==> 1.2.0

23 years agoNew version for UWOBO 1.2.
Claudio Sacerdoti Coen [Tue, 6 Nov 2001 18:46:01 +0000 (18:46 +0000)]
New version for UWOBO 1.2.

23 years ago1) New syntax: methods add, reload and remove can now process multiple
Claudio Sacerdoti Coen [Tue, 6 Nov 2001 18:34:48 +0000 (18:34 +0000)]
1) New syntax: methods add, reload and remove can now process multiple
   entries with just one method invocation. NO BACKWARD COMPATIBILITY RETAINED.
2) Serialization and deserialization: when serialization is enabled, every
   time a stylesheet is recompiled it is also serialized on disk. When
   booting, UWOBO automatically reloads every serialized stylesheet.
3) More verbosity: every method gives back to the user and writes in the log
   much more information than before.
4) Methods update and updateAll (whose semantic was unclear) definitely removed.

23 years agoCommit of Ferruccio changes:
Claudio Sacerdoti Coen [Tue, 6 Nov 2001 12:35:51 +0000 (12:35 +0000)]
Commit of Ferruccio changes:
* New syntax: every method now accepts a list of inputs
* Small bug fixes

23 years agoAlgebra notation.
Andrea Asperti [Mon, 5 Nov 2001 09:06:40 +0000 (09:06 +0000)]
Algebra notation.

23 years agoSmall bug fixed:
Claudio Sacerdoti Coen [Mon, 5 Nov 2001 08:56:25 +0000 (08:56 +0000)]
Small bug fixed:
 * xsl-import not first instruction
 * $id ==> @id

23 years agoSimple stylesheet for Dublin Core Metadata rendering.
Claudio Sacerdoti Coen [Tue, 30 Oct 2001 13:59:30 +0000 (13:59 +0000)]
Simple stylesheet for Dublin Core Metadata rendering.

23 years agoDublin Core Metadata rendering added.
Claudio Sacerdoti Coen [Tue, 30 Oct 2001 13:32:57 +0000 (13:32 +0000)]
Dublin Core Metadata rendering added.

23 years agoVery simple stylesheet to render Dublin Core Metadata.
Claudio Sacerdoti Coen [Tue, 30 Oct 2001 13:32:34 +0000 (13:32 +0000)]
Very simple stylesheet to render Dublin Core Metadata.

23 years agobackpointer ==> backPointer
Claudio Sacerdoti Coen [Mon, 29 Oct 2001 15:56:54 +0000 (15:56 +0000)]
backpointer ==> backPointer

23 years agoNew copyright free implementation of menus in JavaScript.
Claudio Sacerdoti Coen [Sun, 28 Oct 2001 22:48:19 +0000 (22:48 +0000)]
New copyright free implementation of menus in JavaScript.

23 years agoBUG Fixed: arcs with attributes were not processed in the right way.
Claudio Sacerdoti Coen [Sun, 28 Oct 2001 22:46:32 +0000 (22:46 +0000)]
BUG Fixed: arcs with attributes were not processed in the right way.

23 years agoSome comments added.
Claudio Sacerdoti Coen [Fri, 26 Oct 2001 12:14:14 +0000 (12:14 +0000)]
Some comments added.

23 years agoProblem of URLs too long for I.E. avoided by removing an unuseful parameter
Claudio Sacerdoti Coen [Fri, 26 Oct 2001 12:12:10 +0000 (12:12 +0000)]
Problem of URLs too long for I.E. avoided by removing an unuseful parameter
from the inner URL to create a graph. It seems to work for now...

23 years agoSmall bug: the theory was open in the graph windows instead of its own.
Claudio Sacerdoti Coen [Thu, 25 Oct 2001 17:16:40 +0000 (17:16 +0000)]
Small bug: the theory was open in the graph windows instead of its own.

23 years agoForward and backward metadata added to the Raw menu.
Claudio Sacerdoti Coen [Thu, 25 Oct 2001 16:44:28 +0000 (16:44 +0000)]
Forward and backward metadata added to the Raw menu.
OPEN BUG: asking metadata for inductive types does not work. A window
requesting which metadata to show should be opened instead.

23 years agoThere were still many problems with URIs with a ' in the middle.
Claudio Sacerdoti Coen [Thu, 25 Oct 2001 16:36:04 +0000 (16:36 +0000)]
There were still many problems with URIs with a ' in the middle.
Now they should be all resolved (in theory, at least ;-)

23 years agoAlso starting from metadatas it is now possible to select the number
Claudio Sacerdoti Coen [Thu, 25 Oct 2001 16:07:49 +0000 (16:07 +0000)]
Also starting from metadatas it is now possible to select the number
of nodes.

23 years agoClicking on the AREA and not on the menu just pop-ups the menu again instead
Claudio Sacerdoti Coen [Thu, 25 Oct 2001 13:14:47 +0000 (13:14 +0000)]
Clicking on the AREA and not on the menu just pop-ups the menu again instead
of crashing.

23 years agoBUG FIXED: URIs with a ' in the middle do not create problems any more.
Claudio Sacerdoti Coen [Thu, 25 Oct 2001 11:59:16 +0000 (11:59 +0000)]
BUG FIXED: URIs with a ' in the middle do not create problems any more.
[Note: We now have problems with URIs with a " in the middle ;-)]

23 years agoA -> B now means "A depends on B" both in backward and forward graphs
Claudio Sacerdoti Coen [Thu, 25 Oct 2001 10:54:43 +0000 (10:54 +0000)]
A -> B now means "A depends on B" both in backward and forward graphs

23 years agoA link to the theory of backward dependencies added to the menu.
Claudio Sacerdoti Coen [Thu, 25 Oct 2001 10:31:33 +0000 (10:31 +0000)]
A link to the theory of backward dependencies added to the menu.

23 years agoThe code to create a link to the theory automatically generated from the
Claudio Sacerdoti Coen [Thu, 25 Oct 2001 10:27:01 +0000 (10:27 +0000)]
The code to create a link to the theory automatically generated from the
backward metadata has been moved here from metadataLib.xsl.

23 years agoCode clean-up: the code to create the link to the theory automatically
Claudio Sacerdoti Coen [Thu, 25 Oct 2001 10:26:24 +0000 (10:26 +0000)]
Code clean-up: the code to create the link to the theory automatically
generated from the backward metadata has been moved to makeGraphLinks.js

23 years agoThe JavaScript code is now defined in on-line/javascript/graphLinks.xsl and
Claudio Sacerdoti Coen [Thu, 25 Oct 2001 10:20:58 +0000 (10:20 +0000)]
The JavaScript code is now defined in on-line/javascript/graphLinks.xsl and
it is shared with medataLib.xsl.

23 years agoCode obtained from the factorization of makeGraphLinks.xsl and metadataLib.xsl
Claudio Sacerdoti Coen [Thu, 25 Oct 2001 10:19:53 +0000 (10:19 +0000)]
Code obtained from the factorization of makeGraphLinks.xsl and metadataLib.xsl

23 years agoOooops. I have exchanged the targets of the links to the graphs of
Claudio Sacerdoti Coen [Thu, 25 Oct 2001 09:45:52 +0000 (09:45 +0000)]
Oooops. I have exchanged the targets of the links to the graphs of
forward and backward dependencies. Fixed.

23 years agoCode to share with makeGraphLinks.xsl extracted to graphLinks.js
Claudio Sacerdoti Coen [Wed, 24 Oct 2001 17:31:32 +0000 (17:31 +0000)]
Code to share with makeGraphLinks.xsl extracted to graphLinks.js

23 years agoCode of metadataLib.xsl to share with makeGraphLinks.xsl extracted to
Claudio Sacerdoti Coen [Wed, 24 Oct 2001 17:31:30 +0000 (17:31 +0000)]
Code of metadataLib.xsl to share with makeGraphLinks.xsl extracted to
graphLinks.js

23 years agoBug fixed: now links to metadata are created iff at least one pointer is there.
Claudio Sacerdoti Coen [Wed, 24 Oct 2001 16:40:08 +0000 (16:40 +0000)]
Bug fixed: now links to metadata are created iff at least one pointer is there.

23 years agometadataControl and demultiplexMutual merged together into metadataControl
Claudio Sacerdoti Coen [Wed, 24 Oct 2001 16:15:41 +0000 (16:15 +0000)]
metadataControl and demultiplexMutual merged together into metadataControl

23 years agometadataLib2.xsl renamed makeGraphLinks.xsl and committed.
Claudio Sacerdoti Coen [Wed, 24 Oct 2001 15:59:16 +0000 (15:59 +0000)]
metadataLib2.xsl renamed makeGraphLinks.xsl and committed.

23 years agoStylesheet to add links menus to graphs added.
Claudio Sacerdoti Coen [Wed, 24 Oct 2001 15:58:16 +0000 (15:58 +0000)]
Stylesheet to add links menus to graphs added.

23 years agoNew procedure to create metadata committed and old procedure removed.
Claudio Sacerdoti Coen [Wed, 24 Oct 2001 15:33:16 +0000 (15:33 +0000)]
New procedure to create metadata committed and old procedure removed.
The new procedure is based on ocaml code and builds metadata for both
forward and backward pointers. The old one was based on a stylesheet.

23 years agomk_meta_graph.xsl and mk_dep_graph.xsl factorised using
Claudio Sacerdoti Coen [Wed, 24 Oct 2001 15:15:19 +0000 (15:15 +0000)]
mk_meta_graph.xsl and mk_dep_graph.xsl factorised using
mk_meta_and_dep_graph.xsl.

23 years agomk_dep_graph reimplemented using the forward-pointers metadata.
Claudio Sacerdoti Coen [Wed, 24 Oct 2001 14:14:14 +0000 (14:14 +0000)]
mk_dep_graph reimplemented using the forward-pointers metadata.
It is now almost a perfect copy of mk_meta_graph.xsl.

23 years agoRDFURI removed because no more unique.
Claudio Sacerdoti Coen [Wed, 24 Oct 2001 14:11:25 +0000 (14:11 +0000)]
RDFURI removed because no more unique.

23 years agoPorted to RDF syntax.
Claudio Sacerdoti Coen [Wed, 24 Oct 2001 12:44:34 +0000 (12:44 +0000)]
Ported to RDF syntax.

23 years agoPorting to RDF syntax.
Claudio Sacerdoti Coen [Wed, 24 Oct 2001 12:43:40 +0000 (12:43 +0000)]
Porting to RDF syntax.

23 years agoThe cache now supports different RDF URI schema at the same time.
Claudio Sacerdoti Coen [Wed, 24 Oct 2001 10:35:32 +0000 (10:35 +0000)]
The cache now supports different RDF URI schema at the same time.

23 years agotemplate mk-mml-op-noannot was modified to allow hidden parameters
Ferruccio Guidi [Mon, 22 Oct 2001 16:50:56 +0000 (16:50 +0000)]
template mk-mml-op-noannot was modified to allow hidden parameters
eq and eqT where aligned

23 years agoInitial revision
Luca Padovani [Thu, 18 Oct 2001 20:32:41 +0000 (20:32 +0000)]
Initial revision

23 years agoBug fixing: now the link to the graphs produce extended URIs
Claudio Sacerdoti Coen [Thu, 18 Oct 2001 10:17:15 +0000 (10:17 +0000)]
Bug fixing: now the link to the graphs produce extended URIs
(e.g. ".../nat.ind#xpointer(1/1/1")

23 years agomk_dep_graph.xsl now differentiates the constructors from the
Claudio Sacerdoti Coen [Thu, 18 Oct 2001 10:11:28 +0000 (10:11 +0000)]
mk_dep_graph.xsl now differentiates the constructors from the
inductive types producing "extended" URIs
(e.g. ".../nat.ind#xpointer(1/1/1)")

23 years agoOooops. After the last commit all the URLs were damaged.
Claudio Sacerdoti Coen [Wed, 17 Oct 2001 15:34:43 +0000 (15:34 +0000)]
Oooops. After the last commit all the URLs were damaged.

23 years agoMakefile.in that support some new architectures.
Stefano Zacchiroli [Wed, 17 Oct 2001 13:02:20 +0000 (13:02 +0000)]
Makefile.in that support some new architectures.

23 years agoBug removed/Feature changed: CIC URIs for inductive data types
Claudio Sacerdoti Coen [Wed, 17 Oct 2001 10:11:56 +0000 (10:11 +0000)]
Bug removed/Feature changed: CIC URIs for inductive data types
and constructors ending with an #xpointer are now handled
(more) correctly.

23 years agoBug related to #xpointer(1/n/m) constructor URI fixed.
Claudio Sacerdoti Coen [Tue, 16 Oct 2001 16:53:07 +0000 (16:53 +0000)]
Bug related to #xpointer(1/n/m) constructor URI fixed.

23 years agoNew implementation of the graph stuff: now every hard-coded URL has been
Claudio Sacerdoti Coen [Mon, 15 Oct 2001 06:17:02 +0000 (06:17 +0000)]
New implementation of the graph stuff: now every hard-coded URL has been
removed.

23 years agoHelp method added
Claudio Sacerdoti Coen [Mon, 15 Oct 2001 06:16:18 +0000 (06:16 +0000)]
Help method added

23 years agoNew implementation of the graphs stuff: now every hard-coded URL has
Claudio Sacerdoti Coen [Mon, 15 Oct 2001 06:14:13 +0000 (06:14 +0000)]
New implementation of the graphs stuff: now every hard-coded URL has
been removed.

23 years agoCommented code removed
Claudio Sacerdoti Coen [Mon, 15 Oct 2001 06:13:10 +0000 (06:13 +0000)]
Commented code removed

23 years agoNew implementation of the graph staff: the logic has been moved
Claudio Sacerdoti Coen [Fri, 12 Oct 2001 08:42:37 +0000 (08:42 +0000)]
New implementation of the graph staff: the logic has been moved
from mk_html.pl to the stylesheets

23 years agoNew implementation of the graph staff: logic moved
Claudio Sacerdoti Coen [Fri, 12 Oct 2001 08:34:14 +0000 (08:34 +0000)]
New implementation of the graph staff: logic moved
from mk_html.pl to the stylesheets.

23 years agoWhoops. Forgot to open the CIC file in the cic window.
Claudio Sacerdoti Coen [Tue, 9 Oct 2001 16:42:52 +0000 (16:42 +0000)]
Whoops. Forgot to open the CIC file in the cic window.

23 years agoMenu in JavaScript substituted to multi-area links. Cool.
Claudio Sacerdoti Coen [Tue, 9 Oct 2001 16:34:38 +0000 (16:34 +0000)]
Menu in JavaScript substituted to multi-area links. Cool.

23 years agoCode improvement, same functionalities.
Claudio Sacerdoti Coen [Tue, 9 Oct 2001 15:12:10 +0000 (15:12 +0000)]
Code improvement, same functionalities.

23 years agoNew implementation: now the number of nodes is used to prune the graph
Claudio Sacerdoti Coen [Mon, 8 Oct 2001 12:03:05 +0000 (12:03 +0000)]
New implementation: now the number of nodes is used to prune the graph

23 years agocvsignore added
Claudio Sacerdoti Coen [Mon, 8 Oct 2001 12:01:41 +0000 (12:01 +0000)]
cvsignore added

23 years agoFirst release checked in
Claudio Sacerdoti Coen [Mon, 8 Oct 2001 12:00:27 +0000 (12:00 +0000)]
First release checked in

23 years agoNew graph implementation: the visit is no more pruned on a level base, but
Claudio Sacerdoti Coen [Mon, 8 Oct 2001 11:55:24 +0000 (11:55 +0000)]
New graph implementation: the visit is no more pruned on a level base, but
when the number of the nodes in the graph exceeds a fixed limit.

23 years agoDebian packaging of helmpot-0.0.3
Claudio Sacerdoti Coen [Fri, 5 Oct 2001 17:35:13 +0000 (17:35 +0000)]
Debian packaging of helmpot-0.0.3

23 years agoMany more hard-coded links removed.
Claudio Sacerdoti Coen [Thu, 4 Oct 2001 14:47:27 +0000 (14:47 +0000)]
Many more hard-coded links removed.

23 years agoFirst set of hard-coded URLs removed.
Claudio Sacerdoti Coen [Wed, 3 Oct 2001 15:40:58 +0000 (15:40 +0000)]
First set of hard-coded URLs removed.
Still many remaining.

23 years agoAbsolute path removed thanks to a bug-fixing in Uwobo.
Claudio Sacerdoti Coen [Wed, 3 Oct 2001 15:14:08 +0000 (15:14 +0000)]
Absolute path removed thanks to a bug-fixing in Uwobo.
To process this stylesheet, a version of Uwobo >= 1.1.11 is required.

23 years agoFirst implementation of graphs stuff. Working on my notebook,
Claudio Sacerdoti Coen [Mon, 1 Oct 2001 09:52:16 +0000 (09:52 +0000)]
First implementation of graphs stuff. Working on my notebook,
probably not working on-line, yet.

23 years agoNew stylesheets for graphs added
Claudio Sacerdoti Coen [Mon, 1 Oct 2001 09:46:08 +0000 (09:46 +0000)]
New stylesheets for graphs added

23 years agod_c missing
Claudio Sacerdoti Coen [Mon, 1 Oct 2001 09:40:17 +0000 (09:40 +0000)]
d_c missing

23 years agoFirst implementation of graphs. Working on my notebook, probably not
Claudio Sacerdoti Coen [Mon, 1 Oct 2001 09:37:07 +0000 (09:37 +0000)]
First implementation of graphs. Working on my notebook, probably not
on-line.

23 years ago* getter.xsl added
Claudio Sacerdoti Coen [Fri, 14 Sep 2001 13:58:49 +0000 (13:58 +0000)]
* getter.xsl added
  In this stylesheet there is a simple function to make the URL
  of an XML file given its URI. (The URL is used to ask the getter
  to retrieve the file)
* every other stylesheet (but ricerca.xsl that is unused and
  links_library.xsl) has been changed to use the new function
  instead of computing the URL cutting&pasting the same code
  again and again.

23 years agobug fix (helm selection) and new version (sigh)
Luca Padovani [Wed, 29 Aug 2001 20:30:54 +0000 (20:30 +0000)]
bug fix (helm selection) and new version (sigh)

23 years agoProof explosion blocked after lambda-abstractions.
Claudio Sacerdoti Coen [Wed, 29 Aug 2001 15:43:47 +0000 (15:43 +0000)]
Proof explosion blocked after lambda-abstractions.

23 years agoProof explosion improved (= avoided) for:
Claudio Sacerdoti Coen [Wed, 29 Aug 2001 15:16:25 +0000 (15:16 +0000)]
Proof explosion improved (= avoided) for:
 1) Proofs after lambda-introductions (linear proofs)
 2) Proofs after a rewriting step (linear proofs)
 3) Proofs after a letin1 (linear proofs)

23 years ago1. Fixati alcuni problemi di indentazione con le rewrite.
Andrea Asperti [Wed, 29 Aug 2001 11:32:53 +0000 (11:32 +0000)]
1. Fixati alcuni problemi di indentazione con le rewrite.
2. Esplosione in un colpo solo di catene di riscrittura.