--- a/src/Provers/make_elim.ML Fri Dec 30 16:56:59 2005 +0100
+++ b/src/Provers/make_elim.ML Fri Dec 30 16:57:00 2005 +0100
@@ -1,6 +1,6 @@
-(* Title: Provers/make_elim.ML
+(* Title: Provers/make_elim.ML
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 2000 University of Cambridge
Classical version of Tactic.make_elim
@@ -15,34 +15,24 @@
signature MAKE_ELIM_DATA =
sig
- val classical : thm (* (~P ==> P) ==> P *)
+ 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
-local
- val cla_dist_concl = prove_goal (the_context ())
- "[| ~Z_ ==> PROP X_; PROP Y_ ==> Z_; PROP X_ ==> PROP Y_ |] ==> Z_"
- (fn [premx,premz,premy] =>
- ([(rtac Data.classical 1),
- (etac (premx RS premy RS premz) 1)]))
-
+fun make_elim rl =
+ let
fun compose_extra nsubgoal (tha,i,thb) =
- Seq.list_of (bicompose false (false,tha,nsubgoal) i thb)
-
-in
+ Seq.list_of (bicompose false (false,tha,nsubgoal) i thb)
+ val revcut_rl' = Drule.incr_indexes rl revcut_rl
-fun make_elim rl =
- let val revcut_rl' = incr_indexes_wrt [] [] [] [rl] revcut_rl
- fun making (i,rl) =
- case compose_extra 2 (cla_dist_concl,i,rl) of
- [] => rl (*terminates by clash of variables!*)
- | rl'::_ => making (i+1,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;
+ THM _ => Tactic.make_elim rl | Empty => Tactic.make_elim rl;
-end
-
end;