src/Provers/project_rule.ML
changeset 22568 ed7aa5a350ef
parent 20218 be3bfb0699ba
equal deleted inserted replaced
22567:1565d476a9e2 22568:ed7aa5a350ef
    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') = Variable.import true [raw_rule] ctxt;
    40     val ((_, [rule]), ctxt') = Variable.import_thms 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]), _) = Variable.import true [raw_rule] ctxt;
    60     val ((_, [rule]), _) = Variable.import_thms 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;