# HG changeset patch
# User paulson
# Date 962182538 -7200
# Node ID cfc6fecbb1e9979c6c5fb0d28148c212d335010d
# Parent  0bfe5354d5e7c9665ef7266d1a97e8118e250397
uses a supplied version of make_elim for addDs

diff -r 0bfe5354d5e7 -r cfc6fecbb1e9 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Wed Jun 28 10:54:47 2000 +0200
+++ b/src/Provers/classical.ML	Wed Jun 28 10:55:38 2000 +0200
@@ -27,6 +27,7 @@
 
 signature CLASSICAL_DATA =
 sig
+  val make_elim : thm -> thm    (* Tactic.make_elim or a classical version*)
   val mp	: thm    	(* [| P-->Q;  P |] ==> Q *)
   val not_elim	: thm		(* [| ~P;  P |] ==> R *)
   val classical	: thm		(* (~P ==> P) ==> P *)