src/HOL/Prolog/prolog.ML
changeset 32282 853ef99c04cc
parent 32260 eb97888fa422
child 32283 3bebc195c124
equal deleted inserted replaced
32281:750101435f60 32282:853ef99c04cc
    65         all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
    65         all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
    66         imp_conjL RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *)
    66         imp_conjL RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *)
    67         imp_conjR,        (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
    67         imp_conjR,        (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
    68         imp_all];         (* "((!x. D) :- G) = (!x. D :- G)" *)
    68         imp_all];         (* "((!x. D) :- G) = (!x. D :- G)" *)
    69 
    69 
    70 (*val hyp_resolve_tac = FOCUS (fn {prems, ...} =>
    70 (*val hyp_resolve_tac = FOCUS_PREMS (fn {prems, ...} =>
    71                                   resolve_tac (maps atomizeD prems) 1);
    71                                   resolve_tac (maps atomizeD prems) 1);
    72   -- is nice, but cannot instantiate unknowns in the assumptions *)
    72   -- is nice, but cannot instantiate unknowns in the assumptions *)
    73 fun hyp_resolve_tac i st = let
    73 fun hyp_resolve_tac i st = let
    74         fun ap (Const("All",_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a  ,t))
    74         fun ap (Const("All",_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a  ,t))
    75         |   ap (Const("op -->",_)$_$t)    =(case ap t of (k,_,t) => (k,true ,t))
    75         |   ap (Const("op -->",_)$_$t)    =(case ap t of (k,_,t) => (k,true ,t))