]> matita.cs.unibo.it Git - helm.git/log
helm.git
17 years agoMore daemons got rid of (and more extra axioms to be proved).
Claudio Sacerdoti Coen [Mon, 16 Jul 2007 17:35:38 +0000 (17:35 +0000)]
More daemons got rid of (and more extra axioms to be proved).

17 years agoLast daemon killed :-)
Claudio Sacerdoti Coen [Mon, 16 Jul 2007 16:10:40 +0000 (16:10 +0000)]
Last daemon killed :-)

17 years agoOne less daemon (about "update"s).
Claudio Sacerdoti Coen [Mon, 16 Jul 2007 16:07:42 +0000 (16:07 +0000)]
One less daemon (about "update"s).

17 years agoAll sub-proofs about "update" closed.
Claudio Sacerdoti Coen [Mon, 16 Jul 2007 16:04:05 +0000 (16:04 +0000)]
All sub-proofs about "update" closed.

17 years agoassembly.ma splitted into many files
Claudio Sacerdoti Coen [Mon, 16 Jul 2007 14:51:18 +0000 (14:51 +0000)]
assembly.ma splitted into many files

17 years ago* NOT RELEASED YET
Stefano Zacchiroli [Mon, 16 Jul 2007 14:34:55 +0000 (14:34 +0000)]
* NOT RELEASED YET

17 years ago* NOT RELEASED YET
Stefano Zacchiroli [Mon, 16 Jul 2007 14:33:30 +0000 (14:33 +0000)]
* NOT RELEASED YET

17 years agoproper path for ps.gz doc
Stefano Zacchiroli [Mon, 16 Jul 2007 14:30:27 +0000 (14:30 +0000)]
proper path for ps.gz doc

17 years ago texlive-base-bin, texlive-latex-extra
Stefano Zacchiroli [Mon, 16 Jul 2007 14:21:44 +0000 (14:21 +0000)]
texlive-base-bin, texlive-latex-extra

17 years ago - add build-dep for doc generation: graphviz, texlive-latex-recommended,
Stefano Zacchiroli [Mon, 16 Jul 2007 14:17:45 +0000 (14:17 +0000)]
  - add build-dep for doc generation: graphviz, texlive-latex-recommended,

17 years ago - add build-dep for doc generation: graphviz, texlive-latex-base,
Stefano Zacchiroli [Mon, 16 Jul 2007 14:12:20 +0000 (14:12 +0000)]
  - add build-dep for doc generation: graphviz, texlive-latex-base,
    texlive-base-bin

17 years ago* debian/rules
Stefano Zacchiroli [Mon, 16 Jul 2007 14:09:23 +0000 (14:09 +0000)]
* debian/rules
  - build ocamldoc documentation at package build time
  - add build-dep on graphviz

17 years agoinvoke make doc after build to create ocamldoc docs
Stefano Zacchiroli [Mon, 16 Jul 2007 14:05:57 +0000 (14:05 +0000)]
invoke make doc after build to create ocamldoc docs

17 years ago* debian/svn-deblayout
Stefano Zacchiroli [Mon, 16 Jul 2007 13:59:36 +0000 (13:59 +0000)]
* debian/svn-deblayout
  - add repository layout information

17 years ago* rebuild against OCaml 3.10 and ocamlnet 2.2
Stefano Zacchiroli [Mon, 16 Jul 2007 13:56:27 +0000 (13:56 +0000)]
* rebuild against OCaml 3.10 and ocamlnet 2.2
* add preliminary support for cookies (new "cookies" method added to an
  - use ocaml.mk CDBS class
  - add build-dep on camlp4, which is now in a separate package
- bump debhelper dep and compatibility level to 5

17 years ago* debian/*.install.in
Stefano Zacchiroli [Mon, 16 Jul 2007 13:49:22 +0000 (13:49 +0000)]
* debian/*.install.in
  - do not attempt to instal *.ml files in target lib directory since they
    are no longer installed by Makefile

17 years ago* rebuild with OCaml 3.10
Stefano Zacchiroli [Mon, 16 Jul 2007 13:31:55 +0000 (13:31 +0000)]
* rebuild with OCaml 3.10
* bump debhelper deps and compatibility level to 5
  - s/Source-Version/binary:Version

17 years agocorrected axiom mod_plus
Wilmer Ricciotti [Mon, 16 Jul 2007 13:07:53 +0000 (13:07 +0000)]
corrected axiom mod_plus

17 years agonew definitions and new theorems
Ferruccio Guidi [Sat, 14 Jul 2007 14:37:11 +0000 (14:37 +0000)]
new definitions and new theorems

17 years agoMore conjectures closed.
Claudio Sacerdoti Coen [Fri, 13 Jul 2007 22:04:05 +0000 (22:04 +0000)]
More conjectures closed.

17 years ago1. requires the new pretty printer for natural numbers
Claudio Sacerdoti Coen [Fri, 13 Jul 2007 18:08:28 +0000 (18:08 +0000)]
1. requires the new pretty printer for natural numbers
2. important properties of plusbyte proved
3. all important conjectures almost proved

17 years agoDirty patch by Zack: natural numbers of Matita are now pretty-printed as numbers...
Claudio Sacerdoti Coen [Fri, 13 Jul 2007 18:04:35 +0000 (18:04 +0000)]
Dirty patch by Zack: natural numbers of Matita are now pretty-printed as numbers. Eureka.

17 years agoLast crazy commit reverted.
Claudio Sacerdoti Coen [Fri, 13 Jul 2007 09:56:42 +0000 (09:56 +0000)]
Last crazy commit reverted.

17 years agoFinal theorem proved. Many many conjectures left. I am unsure of one of them.
Claudio Sacerdoti Coen [Fri, 13 Jul 2007 08:35:47 +0000 (08:35 +0000)]
Final theorem proved. Many many conjectures left. I am unsure of one of them.

17 years agoThe loop invariant I chosed was not correct!
Claudio Sacerdoti Coen [Thu, 12 Jul 2007 18:38:04 +0000 (18:38 +0000)]
The loop invariant I chosed was not correct!

1. statement to be fixed
2. is the new loop invariant strong enough?
3. lot of daemons here and there
4. two conjectures I am not sure of:
   plusbytenc (x*n) x = byte_of_nat (x*S n)
   plusbytec  (x*n) x = plusbytec (x*S n)

17 years agoGetting close to the final result.
Claudio Sacerdoti Coen [Wed, 11 Jul 2007 17:10:26 +0000 (17:10 +0000)]
Getting close to the final result.
The showstopper now is the GtkMathView/Pango bug!
Moreover, unification has become mostly useless (and rewriting with it).

17 years ago1. loop invariant stated, but not proved
Claudio Sacerdoti Coen [Wed, 11 Jul 2007 14:54:04 +0000 (14:54 +0000)]
1. loop invariant stated, but not proved
2. final theorem stated and proved

17 years agonative dependences fixed
Ferruccio Guidi [Wed, 11 Jul 2007 12:23:14 +0000 (12:23 +0000)]
native dependences fixed

17 years ago1. status factorized out in tick
Claudio Sacerdoti Coen [Wed, 11 Jul 2007 10:52:49 +0000 (10:52 +0000)]
1. status factorized out in tick
2. 0*0=0, 0*2=0, x*1=x, x*2=x+x proved
3. still way too slow!

17 years agoauto new => autobatch
Claudio Sacerdoti Coen [Wed, 11 Jul 2007 09:16:43 +0000 (09:16 +0000)]
auto new => autobatch

17 years agoauto new => autobatch
Claudio Sacerdoti Coen [Wed, 11 Jul 2007 09:11:18 +0000 (09:11 +0000)]
auto new => autobatch

17 years ago0. less nice solution by Enrico reverted
Claudio Sacerdoti Coen [Tue, 10 Jul 2007 22:06:50 +0000 (22:06 +0000)]
0. less nice solution by Enrico reverted
1. some bug fixes in assembly code
2. test program simplified
3. reduction now works as expected, thanks to the new reduction strategy
4. BIG BUG SOMEWHERE: (270 \mod 256) reduces to 14 instead of 4!!!
5. requires primitive addition over exadecimal numbers and bytes to
   avoid representing 0+x as byte_of_nat (nat_of_byte x) that does not
   reduce

17 years agoNew reduction strategy: the new reduction strategy behaves as the previous
Claudio Sacerdoti Coen [Tue, 10 Jul 2007 18:48:14 +0000 (18:48 +0000)]
New reduction strategy: the new reduction strategy behaves as the previous
one (performing both CVN and CBV in parallel), but it is much more lazy.
In particular, unwinding is never performed twice on the same term.
On assembly/assembly.ma this seems to solve every performance problem.
Let's see what happens this night with the benchmarks.

17 years agoLa programmazione funzionale e' come TeX, funziona meglio se la prendi a calci.
Enrico Tassi [Tue, 10 Jul 2007 17:11:56 +0000 (17:11 +0000)]
La programmazione funzionale e' come TeX, funziona meglio se la prendi a calci.

17 years agopersistent inner types are now generated in publishing mode
Ferruccio Guidi [Tue, 10 Jul 2007 15:42:40 +0000 (15:42 +0000)]
persistent inner types are now generated in publishing mode

17 years agofixed a bug in the cleanup ofsedir that was not properly catching #xpointer
Enrico Tassi [Tue, 10 Jul 2007 15:15:33 +0000 (15:15 +0000)]
fixed a bug in the cleanup ofsedir that was not properly catching #xpointer

17 years ago...
Enrico Tassi [Tue, 10 Jul 2007 08:15:09 +0000 (08:15 +0000)]
...

17 years ago1. bug fixed in tick
Enrico Tassi [Mon, 9 Jul 2007 17:47:31 +0000 (17:47 +0000)]
1. bug fixed in tick
2. added notation for some big number
3. the whd CBN is responsible for the huge timing;
   reduce works since it is CVB

17 years agosignal hadler restored after runnig external 'make'
Enrico Tassi [Mon, 9 Jul 2007 14:40:00 +0000 (14:40 +0000)]
signal hadler restored after runnig external 'make'

17 years agoInteresting theorem added (but still to be proved).
Claudio Sacerdoti Coen [Mon, 9 Jul 2007 14:34:57 +0000 (14:34 +0000)]
Interesting theorem added (but still to be proved).

17 years agoadded few more fun to this test
Enrico Tassi [Mon, 9 Jul 2007 13:32:17 +0000 (13:32 +0000)]
added few more fun to this test

17 years agonew configuration file sample
Ferruccio Guidi [Mon, 9 Jul 2007 13:04:18 +0000 (13:04 +0000)]
new configuration file sample

17 years agotassi: ported to the new DB architecture.
Ferruccio Guidi [Mon, 9 Jul 2007 13:01:25 +0000 (13:01 +0000)]
tassi: ported to the new DB architecture.
since the 'user' db is mandatory, a fake one should be provided

17 years agoauto->autobatch
Enrico Tassi [Mon, 9 Jul 2007 09:58:45 +0000 (09:58 +0000)]
auto->autobatch

17 years agoinclusion of div_and_mod
Enrico Tassi [Sat, 7 Jul 2007 11:34:18 +0000 (11:34 +0000)]
inclusion of div_and_mod

17 years agomaxipatch for support of multiple DBs.
Enrico Tassi [Fri, 6 Jul 2007 14:49:47 +0000 (14:49 +0000)]
maxipatch for support of multiple DBs.

new 3 different kind of BD can coexist:
user) the user db, where his stuff is stored
   tables are named foo_user
library) the library db, a read only database where the standard library should be
   installed and that is the target of the publish act
legacy) a legacy database (not mandatory) where really read only data is stored

every db can be implement with an sqlite file or a mysql database.

the default configuration file sets 1 and 2 to be the mysql matita database on mowgli,
thus nothing should change for mowgli users. database 3 is not used if you are on mowgli.

the way it should be used by matita users out of the unibo network is commented in the config file:
1) file://~/.matita/user.db for his development
2) file:///usr/share/matita/metadata.db for the matita precompiled standard library
3) mysql://mowgli.cs.unibo.it for the legacy coq stuff, both queries and xml are fetched trough
   the net

this allows us to really distribute matita in a rather sane way, with a
precompiled library visible systemwide and having all per user data and
metadata in ~/.matita. There is no need for the user to install and configure
mysql, and can use mowgli just decommenting few lines in the config file.

17 years agoExadecimal numbers are now used. This is a great speed-up.
Claudio Sacerdoti Coen [Thu, 5 Jul 2007 21:47:27 +0000 (21:47 +0000)]
Exadecimal numbers are now used. This is a great speed-up.
Moreover, byte_of_nat is now modulo 256. Thus ADDd is now implemented
correctly.

17 years agoExample program executed for x,y=0.
Claudio Sacerdoti Coen [Wed, 4 Jul 2007 22:17:13 +0000 (22:17 +0000)]
Example program executed for x,y=0.
It works (slowly, much slowly)!

17 years agoQuick hack: matita natural numbers are now accepted by the parser/disambiguator.
Claudio Sacerdoti Coen [Wed, 4 Jul 2007 21:36:49 +0000 (21:36 +0000)]
Quick hack: matita natural numbers are now accepted by the parser/disambiguator.
If nat/nat.ma is not compiled yet, I do not know what happens.

17 years agoBug fixed: a ~with_cast is now inserted when appropriate to avoid translation
Claudio Sacerdoti Coen [Wed, 4 Jul 2007 20:19:24 +0000 (20:19 +0000)]
Bug fixed: a ~with_cast is now inserted when appropriate to avoid translation
of a bottom-up conversion into a top-down conversion.

17 years agoIn place of conclude, obtain FIXMEXXX is now generated when required.
Claudio Sacerdoti Coen [Wed, 4 Jul 2007 20:17:47 +0000 (20:17 +0000)]
In place of conclude, obtain FIXMEXXX is now generated when required.

17 years ago1. Code simplification
Claudio Sacerdoti Coen [Wed, 4 Jul 2007 20:16:47 +0000 (20:16 +0000)]
1. Code simplification
2. Bug fixed: do not anticipate justification for rewritingLR or rewriting RL
   if justification is "exact"

17 years agois_top_down was not propageted correctly under a bottom-up conversion.
Claudio Sacerdoti Coen [Wed, 4 Jul 2007 20:15:18 +0000 (20:15 +0000)]
is_top_down was not propageted correctly under a bottom-up conversion.

17 years ago1. "by proof" now allowed as a justification in equality chains.
Claudio Sacerdoti Coen [Wed, 4 Jul 2007 20:13:49 +0000 (20:13 +0000)]
1. "by proof" now allowed as a justification in equality chains.
   It opens a side-proof to be proved immediately.
2. Side proofs restored in equality chains in content2pres.ml

17 years agoAdded ~with_cast to the change tactic.
Claudio Sacerdoti Coen [Wed, 4 Jul 2007 20:12:41 +0000 (20:12 +0000)]
Added ~with_cast to the change tactic.
When with_cast is true, a cast is recorded in the lambda term.

17 years agoBug fixed: name in letin was printed as "previous" even if given.
Claudio Sacerdoti Coen [Wed, 4 Jul 2007 20:05:55 +0000 (20:05 +0000)]
Bug fixed: name in letin was printed as "previous" even if given.

17 years agoMore opcodes (badly) implemented.
Claudio Sacerdoti Coen [Wed, 4 Jul 2007 17:58:08 +0000 (17:58 +0000)]
More opcodes (badly) implemented.

17 years agoList.ma: added function nth (with default value in case of failure)
Claudio Sacerdoti Coen [Wed, 4 Jul 2007 17:12:22 +0000 (17:12 +0000)]
List.ma: added function nth (with default value in case of failure)
Assembly: a toy example on proving properties of assembly programs.
 It should be moved somewhere else. It shows HUGE problems with
 simplification and display of (very very large) terms.

17 years agoNew definition of Euler's totient function.
Cristian Armentano [Sat, 30 Jun 2007 17:15:15 +0000 (17:15 +0000)]
New definition of Euler's totient function.
New theorems about sigma_p (invoked with an always true predicate).
Theorem about the sum of totient invocations on the divisors of a natural number.

17 years agoIn order to generate executable declarative scripts, we are now splitting
Claudio Sacerdoti Coen [Sat, 30 Jun 2007 12:33:24 +0000 (12:33 +0000)]
In order to generate executable declarative scripts, we are now splitting
the "Rewrite" content-level method into "RewriteRL" and "RewriteLR".

17 years agoBug fixed in bottom-up conversion.
Claudio Sacerdoti Coen [Sat, 30 Jun 2007 12:20:10 +0000 (12:20 +0000)]
Bug fixed in bottom-up conversion.
Since the bottom-up conversion body is put in the applicative context and since
applicative contexts get flattened the test for being in a bottom-up conversion
must be rather complex.

17 years agoBU Conversion was not generated for Rels fixed. I wonder why...
Claudio Sacerdoti Coen [Sat, 30 Jun 2007 12:16:20 +0000 (12:16 +0000)]
BU Conversion was not generated for Rels fixed. I wonder why...

17 years agoNicer layout but possibly more bugged.
Claudio Sacerdoti Coen [Sat, 30 Jun 2007 12:11:01 +0000 (12:11 +0000)]
Nicer layout but possibly more bugged.
We need continuations here to do a good job.

17 years agoSpurious "we need to prove" at the beginning of Intros+LetTac are no longer
Claudio Sacerdoti Coen [Sat, 30 Jun 2007 12:10:09 +0000 (12:10 +0000)]
Spurious "we need to prove" at the beginning of Intros+LetTac are no longer
generated.

17 years agogeneric version, specializing generic_sigma_p.ma
Cristian Armentano [Fri, 29 Jun 2007 16:30:31 +0000 (16:30 +0000)]
generic version, specializing generic_sigma_p.ma

17 years agogeneric version
Cristian Armentano [Fri, 29 Jun 2007 14:33:37 +0000 (14:33 +0000)]
generic version

17 years agotheorems about sigma_p proved using sigma_p_gen
Cristian Armentano [Fri, 29 Jun 2007 14:12:07 +0000 (14:12 +0000)]
theorems about sigma_p proved using sigma_p_gen

17 years agosvn:ignore property set
Ferruccio Guidi [Wed, 27 Jun 2007 20:59:41 +0000 (20:59 +0000)]
svn:ignore property set

17 years agonew gcd properties, and theorems for totient, and theorems for totient1
Cristian Armentano [Wed, 27 Jun 2007 18:05:37 +0000 (18:05 +0000)]
new gcd properties, and theorems for totient, and theorems for totient1

--this line, and those below, will be ignored--

M    minus.ma
M    le_arith.ma
M    lt_arith.ma
M    div_and_mod.ma
M    div_and_mod_new.ma
M    orders.ma
A    propr_div_mod_lt_le_totient1_aux.ma
A    gcd_properties1.ma

17 years agosome old auto yurned into autobatch
Ferruccio Guidi [Tue, 26 Jun 2007 17:58:16 +0000 (17:58 +0000)]
some old auto yurned into autobatch

17 years ago(no commit message)
Cristian Armentano [Tue, 26 Jun 2007 08:47:26 +0000 (08:47 +0000)]

17 years agogeneric sommatory.
Cristian Armentano [Tue, 26 Jun 2007 08:14:09 +0000 (08:14 +0000)]
generic sommatory.

17 years agoremoved ugly printings
Enrico Tassi [Sat, 23 Jun 2007 14:31:12 +0000 (14:31 +0000)]
removed ugly printings

17 years agoPoplMark challenge part 1a: new, shorter version w/o equivariance proofs.
Wilmer Ricciotti [Thu, 21 Jun 2007 16:33:15 +0000 (16:33 +0000)]
PoplMark challenge part 1a: new, shorter version w/o equivariance proofs.

17 years agobetter description
Enrico Tassi [Thu, 21 Jun 2007 14:45:04 +0000 (14:45 +0000)]
better description

17 years agobetter description
Enrico Tassi [Thu, 21 Jun 2007 13:09:44 +0000 (13:09 +0000)]
better description

17 years agohere we are, a version that compiles and seems to run
Enrico Tassi [Thu, 21 Jun 2007 12:38:34 +0000 (12:38 +0000)]
here we are, a version that compiles and seems to run

17 years agoIncompatible syntax problem between MySql e Sqlite3 fixed.
Claudio Sacerdoti Coen [Thu, 14 Jun 2007 11:07:45 +0000 (11:07 +0000)]
Incompatible syntax problem between MySql e Sqlite3 fixed.

17 years agocut is now implemented building a letin and not a beta redex
Enrico Tassi [Wed, 13 Jun 2007 13:09:20 +0000 (13:09 +0000)]
cut is now implemented building a letin and not a beta redex

17 years agomany changes:
Enrico Tassi [Wed, 13 Jun 2007 13:01:32 +0000 (13:01 +0000)]
many changes:
1) fixed many bugs and added support for implicit detection in
   cic -> declarative
2) added a tactic to find a proof rewriting n times with a given universe
   used instead of auto_paramodulation in the declarative language
   (here you know that 1 rewriting step with that lemma is enough)
3) added ESCAPE to sql queries using LIKE, to make sqlite and mysql compatible

17 years agosort_new_elems on prop_only
Enrico Tassi [Wed, 6 Jun 2007 17:12:39 +0000 (17:12 +0000)]
sort_new_elems on prop_only

17 years agofixed to allow make-dist
Enrico Tassi [Wed, 6 Jun 2007 13:52:49 +0000 (13:52 +0000)]
fixed to allow make-dist

17 years agoadded doc for compose
Enrico Tassi [Wed, 6 Jun 2007 09:07:33 +0000 (09:07 +0000)]
added doc for compose

17 years agocompose now returns a good metasenv
Enrico Tassi [Wed, 6 Jun 2007 08:35:33 +0000 (08:35 +0000)]
compose now returns a good metasenv

17 years agotentative fix
Enrico Tassi [Mon, 4 Jun 2007 16:06:10 +0000 (16:06 +0000)]
tentative fix

17 years agoAnother optimization, already done for geq.
Claudio Sacerdoti Coen [Mon, 4 Jun 2007 13:24:09 +0000 (13:24 +0000)]
Another optimization, already done for geq.

17 years agoauto proof are printed in procedural style
Enrico Tassi [Mon, 4 Jun 2007 13:02:02 +0000 (13:02 +0000)]
auto proof are printed in procedural style

17 years agonew more flexible compose, see matita/tests/compose.ma for a sample
Enrico Tassi [Mon, 4 Jun 2007 12:20:18 +0000 (12:20 +0000)]
new more flexible compose, see matita/tests/compose.ma for a sample

17 years agowrong assertion was inserted, now just a warning to know when it happens
Enrico Tassi [Sat, 2 Jun 2007 09:38:35 +0000 (09:38 +0000)]
wrong assertion was inserted, now just a warning to know when it happens

17 years agoSome interesting optimizations to prevent many bad checks.
Claudio Sacerdoti Coen [Fri, 1 Jun 2007 22:08:43 +0000 (22:08 +0000)]
Some interesting optimizations to prevent many bad checks.

17 years agoProfiling enabled again.
Claudio Sacerdoti Coen [Fri, 1 Jun 2007 19:32:06 +0000 (19:32 +0000)]
Profiling enabled again.

17 years agoremoved some refinement_toolkit
Enrico Tassi [Fri, 1 Jun 2007 15:05:06 +0000 (15:05 +0000)]
removed some refinement_toolkit

17 years agonew compose tactic, still undocumented.
Enrico Tassi [Fri, 1 Jun 2007 14:58:50 +0000 (14:58 +0000)]
new compose tactic, still undocumented.
moved from library to tactics the code for composing coercions.

17 years agoI do not know why, but
Claudio Sacerdoti Coen [Fri, 1 Jun 2007 13:20:21 +0000 (13:20 +0000)]
I do not know why, but
(Helm_registry.get_list Helm_registry.string "matita.includes")
is extremely slow! Removing it from the inner loop really improves performances!

17 years agohacks for paramodulation declarative proofs
Enrico Tassi [Fri, 1 Jun 2007 07:35:59 +0000 (07:35 +0000)]
hacks for paramodulation declarative proofs

17 years agoFinal (???) bug fixed.
Claudio Sacerdoti Coen [Thu, 31 May 2007 18:04:22 +0000 (18:04 +0000)]
Final (???) bug fixed.
The fixpoint for n=1 is now reached in 22s.

17 years agoDOOMSDAY 1.0:
Claudio Sacerdoti Coen [Thu, 31 May 2007 15:06:22 +0000 (15:06 +0000)]
DOOMSDAY 1.0:
 this is the commit that (partially) allows Matita to understand its own
 output. I.e. the natural language generated is now the declarative language.
 This is probably still highly bugged in most cases.

17 years agoBug fixed: wrong id.
Claudio Sacerdoti Coen [Thu, 31 May 2007 15:02:52 +0000 (15:02 +0000)]
Bug fixed: wrong id.

17 years agoFerruccio has changed the semantics of the old ~pattern argument of elim_tac.
Claudio Sacerdoti Coen [Thu, 31 May 2007 15:02:14 +0000 (15:02 +0000)]
Ferruccio has changed the semantics of the old ~pattern argument of elim_tac.
However, he did not fix by_induction_tac accordingly. For now I comment out
the ~pattern application. To be fixed.

17 years agoMore exceptions pretty-printed.
Claudio Sacerdoti Coen [Thu, 31 May 2007 14:57:52 +0000 (14:57 +0000)]
More exceptions pretty-printed.