src/HOL/HOL.ML
changeset 1485 240cc98b94a7
parent 1465 5d7a7e439cec
child 1515 4ed79ebab64d
     1.1 --- a/src/HOL/HOL.ML	Fri Feb 09 12:18:02 1996 +0100
     1.2 +++ b/src/HOL/HOL.ML	Fri Feb 09 13:41:18 1996 +0100
     1.3 @@ -266,9 +266,32 @@
     1.4  (** Standard abbreviations **)
     1.5  
     1.6  fun stac th = rtac(th RS ssubst);
     1.7 -fun sstac ths = EVERY' (map stac ths);
     1.8  fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); 
     1.9  
    1.10 +(** strip proved goal while preserving !-bound var names **)
    1.11 +
    1.12 +local
    1.13 +
    1.14 +(* work around instantiation bug *)
    1.15 +val myspec = read_instantiate [("P","?XXX")] spec;
    1.16 +val _ $ (_ $ (vx as Var(_,vxT))) = concl_of myspec;
    1.17 +val cvx = cterm_of (#sign(rep_thm myspec)) vx;
    1.18 +val aspec = forall_intr cvx myspec;
    1.19 +
    1.20 +fun specf th a =
    1.21 +  let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),vxT))
    1.22 +  in th RS forall_elim ca aspec end;
    1.23 +
    1.24 +fun spec_mpf th = case concl_of th of
    1.25 +                    _ $ (Const("All",_) $ Abs(a,_,_)) => spec_mpf (specf th a)
    1.26 +                  | _ $ (Const("op -->",_)$_$_) => spec_mpf (th RS mp)
    1.27 +                  | _ => th
    1.28 +
    1.29 +in
    1.30 +
    1.31 +fun qed_spec_mp name = bind_thm(name, spec_mpf(result()));
    1.32 +
    1.33 +end;
    1.34  
    1.35  (*** Load simpdata.ML to be able to initialize HOL's simpset ***)
    1.36