paulson [Thu, 29 Jun 2000 12:16:43 +0200] rev 9188
tidied
paulson [Thu, 29 Jun 2000 12:15:08 +0200] rev 9187
fixed proof to cope with the default of equalityCE instead of equalityE
paulson [Thu, 29 Jun 2000 12:14:45 +0200] rev 9186
now uses equalityCE, which usually is more efficent than equalityE
paulson [Thu, 29 Jun 2000 12:14:04 +0200] rev 9185
weak elimination rules
wenzelm [Wed, 28 Jun 2000 21:15:02 +0200] rev 9184
classical 'elimify' attribute;
kleing [Wed, 28 Jun 2000 19:57:16 +0200] rev 9183
tuned for ProofGeneral 3.2
kleing [Wed, 28 Jun 2000 19:56:21 +0200] rev 9182
tuning, eliminated rev_surj
paulson [Wed, 28 Jun 2000 12:39:30 +0200] rev 9181
fixed some weak elim rules, and tidied
paulson [Wed, 28 Jun 2000 12:34:08 +0200] rev 9180
tidying and unbatchifying
paulson [Wed, 28 Jun 2000 12:16:36 +0200] rev 9179
no longer depends upon a prior "open Ind_Syntax" from elsewhere