src/HOL/HOL.ML
changeset 2562 d571d6660240
parent 2442 6663e0d210b0
child 3003 c5293a17afa6
     1.1 --- a/src/HOL/HOL.ML	Tue Jan 28 16:21:15 1997 +0100
     1.2 +++ b/src/HOL/HOL.ML	Wed Jan 29 15:32:18 1997 +0100
     1.3 @@ -313,7 +313,8 @@
     1.4  fun stac th = CHANGED o rtac (th RS ssubst);
     1.5  fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); 
     1.6  
     1.7 -(** strip proved goal while preserving !-bound var names **)
     1.8 +
     1.9 +(** strip ! and --> from proved goal while preserving !-bound var names **)
    1.10  
    1.11  local
    1.12  
    1.13 @@ -337,21 +338,12 @@
    1.14       _ $ (Const("op -->",_)$_$_) => th RS mp
    1.15    | _ => raise THM("RSmp",0,[th]));
    1.16  
    1.17 +(*Used in qed_spec_mp, etc., which are declared in thy_data.ML*)
    1.18  fun normalize_thm funs =
    1.19  let fun trans [] th = th
    1.20        | trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
    1.21  in trans funs end;
    1.22  
    1.23 -fun qed_spec_mp name =
    1.24 -  let val thm = normalize_thm [RSspec,RSmp] (result())
    1.25 -  in bind_thm(name, thm) end;
    1.26 -
    1.27 -fun qed_goal_spec_mp name thy s p = 
    1.28 -	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goal thy s p));
    1.29 -
    1.30 -fun qed_goalw_spec_mp name thy defs s p = 
    1.31 -	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));
    1.32 -
    1.33  end;
    1.34  
    1.35