equal
deleted
inserted
replaced
1659 s_betapplys Ts (do_term depth Ts t0, map (do_term depth Ts) [t1, t2]) |
1659 s_betapplys Ts (do_term depth Ts t0, map (do_term depth Ts) [t1, t2]) |
1660 else |
1660 else |
1661 do_term depth Ts |
1661 do_term depth Ts |
1662 (Const (@{const_name prod}, T1 --> range_type T2 --> T3) |
1662 (Const (@{const_name prod}, T1 --> range_type T2 --> T3) |
1663 $ t1 $ incr_boundvars ~1 t2') |
1663 $ t1 $ incr_boundvars ~1 t2') |
|
1664 | Const (@{const_name Set.member}, _) $ t1 |
|
1665 $ (Const (@{const_name Collect}, _) $ t2) => do_term depth Ts (t2 $ t1) |
1664 | Const (x as (@{const_name distinct}, |
1666 | Const (x as (@{const_name distinct}, |
1665 Type (@{type_name fun}, [Type (@{type_name list}, [T']), _]))) |
1667 Type (@{type_name fun}, [Type (@{type_name list}, [T']), _]))) |
1666 $ (t1 as _ $ _) => |
1668 $ (t1 as _ $ _) => |
1667 (t1 |> HOLogic.dest_list |> distinctness_formula T' |
1669 (t1 |> HOLogic.dest_list |> distinctness_formula T' |
1668 handle TERM _ => do_const depth Ts t x [t1]) |
1670 handle TERM _ => do_const depth Ts t x [t1]) |