equal
deleted
inserted
replaced
464 |> map prep_binder |
464 |> map prep_binder |
465 |> fold_union |
465 |> fold_union |
466 |> mk_perm (Bound 0) |
466 |> mk_perm (Bound 0) |
467 |
467 |
468 val goal = mk_fresh_star lhs rhs |
468 val goal = mk_fresh_star lhs rhs |
469 |> (fn t => HOLogic.mk_exists ("p", @{typ perm}, t)) |
469 |> mk_exists ("p", @{typ perm}) |
470 |> HOLogic.mk_Trueprop |
470 |> HOLogic.mk_Trueprop |
471 |
471 |
472 val ss = bn_finite_thms @ @{thms supp_Pair finite_supp finite_sets_supp} |
472 val ss = bn_finite_thms @ @{thms supp_Pair finite_supp finite_sets_supp} |
473 @ @{thms finite.intros finite_Un finite_set finite_fset} |
473 @ @{thms finite.intros finite_Un finite_set finite_fset} |
474 in |
474 in |