equal
deleted
inserted
replaced
296 (** some logic operations **) |
296 (** some logic operations **) |
297 |
297 |
298 (* decompses a formula into params, premises and a conclusion *) |
298 (* decompses a formula into params, premises and a conclusion *) |
299 fun strip_full_horn trm = |
299 fun strip_full_horn trm = |
300 let |
300 let |
301 fun strip_outer_params (Const ("all", _) $ Abs (a, T, t)) = strip_outer_params t |>> cons (a, T) |
301 fun strip_outer_params (Const (@{const_name Pure.all}, _) $ Abs (a, T, t)) = |
|
302 strip_outer_params t |>> cons (a, T) |
302 | strip_outer_params B = ([], B) |
303 | strip_outer_params B = ([], B) |
303 |
304 |
304 val (params, body) = strip_outer_params trm |
305 val (params, body) = strip_outer_params trm |
305 val (prems, concl) = Logic.strip_horn body |
306 val (prems, concl) = Logic.strip_horn body |
306 in |
307 in |