src/Provers/project_rule.ML
changeset 19897 fe661eb3b0e7
parent 19874 cc4b2b882e4c
child 19905 7f480338b66e
equal deleted inserted replaced
19896:286d950883bc 19897:fe661eb3b0e7
    35       | proj k th = proj (k - 1) (conj2 th);
    35       | proj k th = proj (k - 1) (conj2 th);
    36     fun prems k th =
    36     fun prems k th =
    37       (case try imp th of
    37       (case try imp th of
    38         NONE => (k, th)
    38         NONE => (k, th)
    39       | SOME th' => prems (k + 1) th');
    39       | SOME th' => prems (k + 1) th');
    40     val ([rule], ctxt') = ProofContext.import true [raw_rule] ctxt;
    40     val ([rule], ctxt') = Variable.import true [raw_rule] ctxt;
    41     fun result i =
    41     fun result i =
    42       rule
    42       rule
    43       |> proj i
    43       |> proj i
    44       |> prems 0 |-> (fn k =>
    44       |> prems 0 |-> (fn k =>
    45         Thm.permute_prems 0 (~ k)
    45         Thm.permute_prems 0 (~ k)
    55   let
    55   let
    56     fun projs k th =
    56     fun projs k th =
    57       (case try conj2 th of
    57       (case try conj2 th of
    58         NONE => k
    58         NONE => k
    59       | SOME th' => projs (k + 1) th');
    59       | SOME th' => projs (k + 1) th');
    60     val ([rule], _) = ProofContext.import true [raw_rule] ctxt;
    60     val ([rule], _) = Variable.import true [raw_rule] ctxt;
    61   in projects ctxt (1 upto projs 1 rule) raw_rule end;
    61   in projects ctxt (1 upto projs 1 rule) raw_rule end;
    62 
    62 
    63 end;
    63 end;