wenzelm [Thu, 29 Jun 2000 22:31:53 +0200] rev 9195
fixed is_semicolon (keyword instead of command!);
wenzelm [Thu, 29 Jun 2000 22:31:29 +0200] rev 9194
added add_method;
wenzelm [Thu, 29 Jun 2000 22:31:12 +0200] rev 9193
have_theorems etc.: handle multiple lists of arguments;
added method_setup;
wenzelm [Thu, 29 Jun 2000 22:29:46 +0200] rev 9192
have_thmss: handle multiple lists of arguments;
paulson [Thu, 29 Jun 2000 16:50:52 +0200] rev 9191
now freezes Vars in order to prevent errors in cases like these:
Goal "Suc (x + i + j) + ?q ?ii ?jj + k + x = xxx";
Goal "Suc (x + i + j) = x + f(?q i j) + k";
Goal "Suc (x + i + j) = x + ?q i j + k";
Goal "Suc (?q ?ii ?jj + i + j) + ?rq ?ii ?jj + k + ?q ?ii ?jj = xxx";
paulson [Thu, 29 Jun 2000 12:19:27 +0200] rev 9190
tidied proofs using default rule equalityCE
paulson [Thu, 29 Jun 2000 12:17:18 +0200] rev 9189
the default equalityCE simplifies proofs
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
paulson [Wed, 28 Jun 2000 12:15:56 +0200] rev 9178
fixed some weak elim rules, and tidied
paulson [Wed, 28 Jun 2000 12:15:28 +0200] rev 9177
fixed some weak elim rules
paulson [Wed, 28 Jun 2000 11:00:13 +0200] rev 9176
simplified slightly by using dependencies better in theories
paulson [Wed, 28 Jun 2000 10:58:06 +0200] rev 9175
finally theory Bin (the integers) is included
paulson [Wed, 28 Jun 2000 10:57:35 +0200] rev 9174
FORCED TO RENAME "W" DUE TO COMPOSE VARIABLE-CLASH BUG
paulson [Wed, 28 Jun 2000 10:56:34 +0200] rev 9173
fixed some weak elim rules
paulson [Wed, 28 Jun 2000 10:56:01 +0200] rev 9172
implements a classical version of make_elim
paulson [Wed, 28 Jun 2000 10:55:38 +0200] rev 9171
uses a supplied version of make_elim for addDs
paulson [Wed, 28 Jun 2000 10:54:47 +0200] rev 9170
warns of weak elim rules and ignores them
paulson [Wed, 28 Jun 2000 10:54:21 +0200] rev 9169
tidying and unbatchifying
paulson [Wed, 28 Jun 2000 10:52:02 +0200] rev 9168
fixed some abuses of addDs and addEs