# HG changeset patch
# User wenzelm
# Date 1136062175 -3600
# Node ID 85e7f80023fc23bb8231fdbb7504d0373bfeca7a
# Parent  88abdee3e23fbaca51d47d0b28242ab5cf6442db
obsolete, see classical_rule in Provers/classical.ML;

diff -r 88abdee3e23f -r 85e7f80023fc src/Provers/make_elim.ML
--- a/src/Provers/make_elim.ML	Sat Dec 31 13:03:55 2005 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-(*  Title:      Provers/make_elim.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   2000  University of Cambridge
-
-Classical version of Tactic.make_elim
-
-In classical logic, we can make stronger elimination rules using this version.
-For instance, the HOL rule injD is transformed into
-    [| inj ?f; ~ ?W ==> ?f ?x = ?f ?y; ?x = ?y ==> ?W |] ==> ?W
-while Tactic.make_elim would yield the weaker rule
-    [| inj ?f; ?f ?x = ?f ?y; ?x = ?y ==> PROP ?W |] ==> PROP ?W
-Such rules can cause Fast_tac to fail and Blast_tac to report "PROOF FAILED"
-*)
-
-signature MAKE_ELIM_DATA =
-sig
-  val cla_dist_concl: thm  (*"[| ~Z ==> PROP X; PROP Y ==> Z;  PROP X ==> PROP Y |] ==> Z"*)
-end;
-
-functor Make_Elim_Fun(Data: MAKE_ELIM_DATA)  =
-struct
-
-fun make_elim rl =
-  let
-    fun compose_extra nsubgoal (tha,i,thb) =
-      Seq.list_of (bicompose false (false,tha,nsubgoal) i thb)
-    val revcut_rl' = Drule.incr_indexes rl revcut_rl
-
-    fun making (i,rl) =
-      case compose_extra 2 (Data.cla_dist_concl,i,rl) of
-        [] => rl     (*terminates by clash of variables!*)
-      | rl'::_ => making (i+1,rl')
-    in  making (2, hd (compose_extra 1 (rl, 1, revcut_rl')))  end
-    handle (*in default, use the previous version, which never fails*)
-      THM _ => Tactic.make_elim rl | Empty => Tactic.make_elim rl;
-
-end;