equal
deleted
inserted
replaced
36 Join(Assumption arg,[]) :: rev_deriv der |
36 Join(Assumption arg,[]) :: rev_deriv der |
37 | rev_deriv (Join (Bicompose arg, [rder, sder])) = |
37 | rev_deriv (Join (Bicompose arg, [rder, sder])) = |
38 Join (Bicompose arg, linear rder) :: rev_deriv sder |
38 Join (Bicompose arg, linear rder) :: rev_deriv sder |
39 | rev_deriv (Join (_, [der])) = rev_deriv der |
39 | rev_deriv (Join (_, [der])) = rev_deriv der |
40 | rev_deriv (Join (rl, der::ders)) = (*catch-all case; doubtful?*) |
40 | rev_deriv (Join (rl, der::ders)) = (*catch-all case; doubtful?*) |
41 Join(rl, flat (map linear ders)) :: rev_deriv der |
41 Join(rl, List.concat (map linear ders)) :: rev_deriv der |
42 and linear der = rev (rev_deriv der); |
42 and linear der = rev (rev_deriv der); |
43 |
43 |
44 |
44 |
45 (*** Conversion of object-level proof trees ***) |
45 (*** Conversion of object-level proof trees ***) |
46 |
46 |